La prochaine session du séminaire « Réflexions » se tiendra le vendredi 20 mars 2026, de 13h30 à 17h30, dans la salle de conférences de l’Institut Élie Cartan de Lorraine (plan d’accès : https://iecl.univ-lorraine.fr/plan-dacces/). La session se composera de deux exposés de 13h30 à 15h30 et d’une session pratique de 16h à 17h30. Vous pouvez assister à l’ensemble de la session ou à l’une des deux parties seulement.

En voici le programme :

— 13h30-14h30 — exposé d’Antoine Chambert-Loir (Institut de mathématiques de Jussieu – Paris Rive Gauche, Université Paris Cité) : Retour d’expérience en mathématiques formalisées

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.

— 14h30-15h30 — exposé de Yacin Hamami (Archives Henri-Poincaré, CNRS) : Démonstrations, scripts, et preuves formelles : Quels liens entre l’idéal et la pratique de la démonstration ?

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. 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.

— 16h-17h30 — session pratique « Math en Lean » animée par Vincent Trélat et 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 et Patrick Massot (https://leanprover-community.github.io/mathematics_in_lean/index.html), avec l’appui 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 si vous souhaitez le finir.

Tout le monde est bienvenu à l’une ou l’autre des activités.

Les prochaines sessions auront lieu :

•     Vendredi 3 avril, aux Archives Henri Poincaré : Philippe de Groote (Loria) et Baptiste Mélès (Archives Henri Poincaré)

Le séminaire Réflexions est organisé conjointement par les Archives Henri Poincaré, l’Institut Élie Cartan de Lorraine et le Loria (laboratoire lorrain de recherche en informatique et ses applications).

Les organisateurs pour cette année sont Alexandre Afgoustidis (IECL), Alain Genestier (IECL), Yacin Hamami (AHP) et Sophie Tourret (LORIA).

——————————

The next session of the Réflexions seminar will be held on Friday, March 20, 2026, from 1:30 p.m. to 5:30 p.m., in the conference room of the Institut Élie Cartan de Lorraine (map: https://iecl.univ-lorraine.fr/plan-dacces/). The session will consist of two talks from 1:30 p.m. to 3:30 p.m. and a practical session from 4:00 p.m. to 5:30 p.m. You can attend the entire session or just one of the two parts.

Here is the program (for the abstracts see the French version above):

— 1:30–2:30 p.m. — talk by Antoine Chambert-Loir (Institut de mathématiques de Jussieu – Paris Rive Gauche, Université Paris Cité): Retour d’expérience en mathématiques formalisées

— 2:30–3:30 p.m. — talk by Yacin Hamami (Archives Henri-Poincaré, CNRS): Démonstrations, scripts, et preuves formelles : Quels liens entre l’idéal et la pratique de la démonstration ?

— 4:00–5:30 p.m. — practice session « Math in Lean » by Vincent Trélat and Ghilain Bergeron (Loria)

Here is the program for the sessions after that one:

•     Friday, April 3, Archives Henri Poincaré: Philippe de Groote (Loria) and Baptiste Mélès (Archives Henri Poincaré)