Program
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
Talk
First Speaker: Antoine Chambert-Loir (Institut de mathématique de Jussieu – Paris Rive Gauche)
Title: TBA
Abstract: TBA
Second Speaker: Yacin Hamami (Archives Henri-Poincaré)
Title: Philosophical conceptions of mathematical rigor
Abstract: TBA
Practice Session “Math in LEAN”
Continuation of the previous practice session.
Location: TBA
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).