The seminar Reflexions is a new joint seminar between the Institut Élie Cartan de Lorraine (IECL), the Archives Henri-Poincaré (AHP), and the Lorraine Research Laboratory in Computer Science and its Applications (Loria) at the Université de Lorraine.
It consists of general-interest talks and activities intended for a broad audience, centered on a single yearly theme. The theme is chosen for its common interest to members of our three institutes, and for its potential to foster exchanges of ideas and viewpoints across backgrounds.
The theme for the Spring 2026 is Proofs, rigor, and formalization.
In the past few years, proof assistants have generated intense interest and curiosity among mathematicians and philosophers. By proof assistants, we mean computer-assisted tools for the verification of classical proofs. What are these tools? How do they work? What are their strengths and weaknesses? What impact can they have on the practice of mathematical proofs, and on our conceptions of the notion of rigor in mathematics?
These and related questions will be discussed through talks, practice sessions, discussion sessions, and more.
We shall meet six Friday afternoons during the first semester of 2026. Below is the program for the first four sessions. The next sessions will be held after May 15 and will be announced soon.
Session 1 — IECL — Friday, February 6, 2026
13h30-14h45: Talk
Speaker: Patrick Massot (Laboratoire de mathématique d’Orsay)
Title: Pourquoi raconter des maths aux ordinateurs ?
Abstract: Dans cet exposé j’expliquerai ce que signifie « expliquer des mathématiques à un ordinateur » et pourquoi je trouve cela intéressant et utile. Je montrerai à quoi ressemble concrètement l’utilisation d’un logiciel permettant d’encoder informatiquement des définitions, énoncés et démonstrations. Je présenterai les applications de ces techniques pour vérifier, expliquer, enseigner ou créer des mathématiques. Je mentionnerai des exemples de projets non-triviaux dans ce domaine et j’évoquerai brièvement les liens avec l’IA. Il n’y a aucun pré-requis.
15h00-17h30: Practice Session
Title: Introduction à l’assistant de preuve Lean par la pratique
Le logiciel Lean permet de parler de maths de tout niveau à son ordinateur. Il peut aussi servir à enseigner le raisonnement mathématique rigoureux, par exemple en L1. Ce TP sera une introduction à l’utilisation de Lean en pratique. Il n’y a aucun pré-requis si ce n’est de venir avec un ordinateur portable.
Location: Salle de Conférence de l’IECL, Faculté des Sciences et technologie Campus, Boulevard des Aiguillettes, 54506 Vandoeuvre-lès-Nancy plan d’accès.
Session 2 — IECL — Friday, March 13, 2026
Talk
Speaker: Sophie Tourret (Loria)
Title: L’automatisation dans les assistants de preuve
Abstract: Pour faire prouver des théorèmes à un ordinateur, il y a deux approche possible :
- la preuve interactive, où l’humain décris les théorèmes et les étapes des preuves à un assistant à la preuve, et
- la preuve automatique, où l’humain fournis simplement les théorèmes encodés sous formes de formules logique, et laisse le prouveur raisonner à sa façon.
Dans cette présentation, je vous exposerai plusieurs techniques de preuve automatique et je vous parlerai de leurs usages dans les assistants de preuve.
Practice Session “Math in LEAN”
Tutors: Vincent Trélat and Ghilain Bergeron (Loria)
Cette session pratique se veut le prolongement de la précédente et proposera aux participants de se plonger dans l’ouvrage Mathematics in Lean de Jeremy Avigad and Patrick Massot (disponible en ligne ici), avec l’appuie d’utilisateurs Lean expérimentés. Il vous sera aussi possible de reprendre le tutoriel de Patrick Massot si vous avez manqué la session précédente ou que vous souhaitez le finir.
Location: Salle de Conférence de l’IECL, Faculté des Sciences et technologie Campus, Boulevard des Aiguillettes, 54506 Vandoeuvre-lès-Nancy plan d’accès.
Session 3 — IECL — Friday, March 20, 2026
Talks
First Speaker: Antoine Chambert-Loir (Institut de mathématique de Jussieu – Paris Rive Gauche, Université Paris Cité)
Title: Retour d’expérience en mathématiques formalisées
Abstract: Pourquoi vouloir faire des preuves formelles ? Qu’apporte l’ordinateur ? Et de quelles preuves parlerait-on ?
À partir de mon expérience des cinq dernières années, qui concerne essentiellement des questions d’algèbre,
j’essayerai de présenter mes bouts de réponse à ces questions.
Second Speaker: Yacin Hamami (Archives Henri-Poincaré, CNRS)
Title: Démonstrations, scripts, et preuves formelles :
Quels liens entre l’idéal et la pratique de la
démonstration ?
Abstract: La formalisation des mathématiques par les assistants de preuve nous confronte à trois types d’objets aux statuts distincts : les démonstrations telles qu’elles figurent dans la pratique ordinaire, adressées à des lecteurs humains qu’elles visent à convaincre et à faire comprendre ; les preuves formelles, objets logiques entièrement explicites que la machine vérifie mécaniquement mais qui restent le plus souvent illisibles pour un lecteur humain ; et entre les deux, les scripts de code rédigés dans des assistants comme Lean, Coq ou Isabelle—objets hybrides qui portent encore la marque des intentions de celui qui les écrit, tout en étant destinés à guider la machine vers une vérification formelle.
Quelle est la nature de ces trois objets, et quelles relations entretiennent-ils entre eux ? Cette question a fait l’objet de débats intenses en philosophie des mathématiques ces dernières années. Au cœur de ces débats se trouve la relation entre les démonstrations dans la pratique et l’idéal de preuve formelle, et en particulier la question de la rigueur mathématique qu’elle soulève. Doit-on concevoir la rigueur des démonstrations en pratique comme reposant, en dernière instance, sur la notion de preuve formelle—une démonstration étant rigoureuse lorsqu’elle est, en principe, formalisable ? Ou doit-on au contraire concevoir la rigueur en pratique comme relativement indépendante de cet idéal, obéissant à des normes et des standards qui lui sont propres ?
Dans cet exposé, je présenterai quelques éléments clés de ces débats ainsi que les principales réponses philosophiques qui ont été proposées.
Practice Session “Math in LEAN”
Tutors: Vincent Trélat and Ghilain Bergeron (Loria)
Cette session pratique se veut le prolongement de la précédente et proposera aux participants de se plonger dans l’ouvrage Mathematics in Lean de Jeremy Avigad and Patrick Massot (disponible en ligne ici), avec l’appuie d’utilisateurs Lean expérimentés.
Location: Salle de Conférence de l’IECL, Faculté des Sciences et technologie Campus, Boulevard des Aiguillettes, 54506 Vandoeuvre-lès-Nancy plan d’accès.
Session 4 — TBA - Friday, April 3, 2026
Talks
First Speaker: Baptiste Mélès (Archives Henri-Poincaré)
Title: TBA
Abstract: TBA
Second Speaker: Philippe de Groote (Loria)
Title: TBA
Abstract: TBA
Round Table
Location: TBA
Session 5 — TBA - TBA
Session 6 — TBA - TBA
Participation
The seminar is open to everyone (students, PhD candidates, researchers, colleagues from neighboring disciplines, etc.).
For any question, please write to the organizers.
Organizers
Acknowledgement and Support
Reflexions is funded by the Institut Élie Cartan de Lorraine (IECL), the Archives Henri-Poincaré (AHP), and the Lorraine Research Laboratory in Computer Science and its Applications (Loria).