Journées mathématiques X-UPS

16 avr. 2026, 10:00 → 17 avr. 2026, 17:30 Europe/Paris

Amphithéâtre Poisson (École polytechnique)

                               Vérification formelle de preuves

                                               Journées mathématiques X-UPS 2026

Conférenciers

• Sébastien Gouëzel, CNRS - IRMAR (Rennes)
• Patrick Massot, Université Paris-Saclay (Orsay)
• Micaela Mayero, Université Sorbonne Paris Nord (Villetaneuse)
• Benjamin Werner, INRIA & École polytechnique (Palaiseau)

Organisateurs scientifiques

• Guillaume Dubach
• Pascale Harinck
• Alain Plagne
• Claude Sabbah

Présentation du thème

Les journées X-UPS 2026 auront pour thème la vérification formelle des preuves mathématiques au moyen de logiciels tels que Lean, Rocq, Isabelle, ou HOL pour ne citer que les plus connus. Différentes facettes de ce thème seront abordés par nos orateurs: aspects théoriques (fonctionnement de ces logiciels et fondements mathématiques impliqués, tels que la théorie des types dépendants utilisée par Lean et Rocq), aspects pragmatiques (réflexion sur la place de cet outil dans l'enseignement des mathématiques et dans la recherche actuelle) et aspetcts historiques (par exemple la célèbre preuve du théorème des quatre couleurs par George Gonthier et Benjamin Werner avec Rocq, anciennement nommé Coq, ou plus récemment le rôle joué par Lean dans le Liquid Tensor Experiment sous l'impulsion de Peter Scholze et Kevin Buzzard). Nos orateurs ont été choisis pour la pertinence et la diversité de leurs expertises avec ces logiciels: Sébastien Gouëzel et Patrick Massot sont des contributeurs actifs de la libraire mathlib de Lean; Benjamin Werner et Micaela Mayero se sont illustrés par leurs travaux avec le logiciel Rocq. 

Présentation des journées

Les journées mathématiques X-UPS sont un stage de formation organisé par le Centre de mathématiques Laurent Schwartz de l'École polytechnique à l'intention des professeurs des classes préparatoires aux grandes écoles scientifiques.        
Elles se tiennent tous les ans au printemps. L'inscription est gratuite mais obligatoire.        
L'objectif est double : d'une part satisfaire l'intérêt des professeurs pour l'actualité de la recherche en mathématiques et en informatique, d'autre part leur apporter des connaissances utilisables dans leur enseignement.        
Le stage comporte six ou sept conférences éventuellement accompagnées de démonstrations ou de travaux pratiques sur ordinateur. Nous souhaitons une participation active des stagiaires sous forme de discussion et questions aux conférenciers.

Les Journées mathématiques X-UPS bénéficient du soutien de la fondation mathématique Jacques Hadamard (FMJH)

jeu. 16 avril

10:00 Café d'accueil

1 Des assistants de preuves pour l’analyse réelle et numérique; un focus sur Rocq: de la recherche à l’enseignement et vice versa (1)

Les outils de preuves formelles, issus des recherches en logique, ont pris de l’ampleur ces dernières décennies. Nous présenterons succinctement ces outils, leurs évolutions ainsi que leurs fondements théoriques.
Les preuves formelles sont utilisées et développées à la fois dans le domaine de l’enseignement, principalement en mathématiques et en informatique, et de la recherche, et ces dernières années, parfois de manière coordonnée.
Nous présenterons ces deux aspects en faisant un focus sur l’analyse réelle et l’analyse numérique en Rocq. Nous nous appuierons régulièrement sur des exemples.

Orateur: Micaela Mayero (Université Sorbonne Paris Nord)

12:00 Discussion - Pause

12:30 Déjeuner

2 Du calcul et des machines dans les preuves (1)

L’ordinateur est une machine capable d’exécuter précisément un algorithme donné. Cela en fait naturellement un outil mathématique. Je parlerai en particulier de deux rôles:
- Vérifier des preuves formelles. C’est le principe des assistants de preuves qui sont le thème de ces journées.
- Effectuer des calculs complexes, numériques ou symboliques, qui sont hors de portée de l’humain.
Nous regarderons comment certains formalismes, comme la théorie des types sous-jacente à Rocq et Lean, permet de concilier ces deux aspects à travers des preuves comportant une part de calcul importante.
Parmi ces preuves, il y a le théorème des quatre couleurs, dont nous présenterons quelques aspects.
Dans une dernière partie, je présenterai des travaux plus récents sur une interface graphique et gestuelle pour construire des preuves formelles de manières (parfois) plus rapide ou intuitive. Ces travaux ouvrant, je l’espère, des pistes nouvelles pour la pédagogie des mathématiques.

Orateur: Benjamin Werner (INRIA & École polytechnique)

15:00 Discussion - Pause

3 Une présentation de Lean et Mathlib à base d'exemples mathématiques (1)

Les assistants de preuve sont des langages dans lesquels on explique à un ordinateur des preuves mathématiques,
l'ordinateur se chargeant de vérifier que le passage d'une ligne à la suivante respecte toujours les règles de la logique. Cela permet
entre autres avantages de garantir quasiment à 100% la correction des démonstrations.

Je présenterai l'assistant de preuves Lean et sa bibliothèque de mathématiques formalisées Mathlib, avec un point de vue de mathématicien praticien
(et donc sans parler du tout du fonctionnement interne des assistants de preuve) :
quelles différences de point de vue faut-il avoir quand on démontre un résultat sur papier ou quand on le formalise, quels sont les types d'arguments les plus
difficiles de chaque côté, quels sont les écueils à éviter, etc.

Je m'appuierai principalement sur des exemples concrets. Je démontrerai puis expliquerai la formalisation d'un théorème sur les vecteurs de translation asymptotique de fonctions 1-lipschitziennes.
Ensuite, je me concentrerai sur la notion de fonction $C^n$, telle qu'exposée dans les livres ou dans les cours, puis telle que formalisée dans Mathlib -- il y a des différences significatives entre les deux,
qui illustrent bien les particularités des mathématiques formalisées.

Orateur: Sébastien Gouézel (CNRS - IRMAR)

ven. 17 avril

4 Des assistants de preuves pour l’analyse réelle et numérique; un focus sur Rocq: de la recherche à l’enseignement et vice versa (2)

Les outils de preuves formelles, issus des recherches en logique, ont pris de l’ampleur ces dernières décennies. Nous présenterons succinctement ces outils, leurs évolutions ainsi que leurs fondements théoriques.
Les preuves formelles sont utilisées et développées à la fois dans le domaine de l’enseignement, principalement en mathématiques et en informatique, et de la recherche, et ces dernières années, parfois de manière coordonnée.
Nous présenterons ces deux aspects en faisant un focus sur l’analyse réelle et l’analyse numérique en Rocq. Nous nous appuierons régulièrement sur des exemples.

Orateur: Micaela Mayero (Université Sorbonne Paris Nord)

10:30 Discussion - Pause

5 Du calcul et des machines dans les preuves (2)

L’ordinateur est une machine capable d’exécuter précisément un algorithme donné. Cela en fait naturellement un outil mathématique. Je parlerai en particulier de deux rôles:
- Vérifier des preuves formelles. C’est le principe des assistants de preuves qui sont le thème de ces journées.
- Effectuer des calculs complexes, numériques ou symboliques, qui sont hors de portée de l’humain.
Nous regarderons comment certains formalismes, comme la théorie des types sous-jacente à Rocq et Lean, permet de concilier ces deux aspects à travers des preuves comportant une part de calcul importante.
Parmi ces preuves, il y a le théorème des quatre couleurs, dont nous présenterons quelques aspects.
Dans une dernière partie, je présenterai des travaux plus récents sur une interface graphique et gestuelle pour construire des preuves formelles de manières (parfois) plus rapide ou intuitive. Ces travaux ouvrant, je l’espère, des pistes nouvelles pour la pédagogie des mathématiques.

Orateur: Benjamin Werner (INRIA & École polytechnique)

12:00 Discussion - Pause

12:30 Déjeuner

6 Une présentation de Lean et Mathlib à base d'exemples mathématiques (2)

Les assistants de preuve sont des langages dans lesquels on explique à un ordinateur des preuves mathématiques,
l'ordinateur se chargeant de vérifier que le passage d'une ligne à la suivante respecte toujours les règles de la logique. Cela permet
entre autres avantages de garantir quasiment à 100% la correction des démonstrations.

Je présenterai l'assistant de preuves Lean et sa bibliothèque de mathématiques formalisées Mathlib, avec un point de vue de mathématicien praticien
(et donc sans parler du tout du fonctionnement interne des assistants de preuve) :
quelles différences de point de vue faut-il avoir quand on démontre un résultat sur papier ou quand on le formalise, quels sont les types d'arguments les plus
difficiles de chaque côté, quels sont les écueils à éviter, etc.

Je m'appuierai principalement sur des exemples concrets. Je démontrerai puis expliquerai la formalisation d'un théorème sur les vecteurs de translation asymptotique de fonctions 1-lipschitziennes.
Ensuite, je me concentrerai sur la notion de fonction $C^n$, telle qu'exposée dans les livres ou dans les cours, puis telle que formalisée dans Mathlib -- il y a des différences significatives entre les deux,
qui illustrent bien les particularités des mathématiques formalisées.

Orateur: Sébastien Gouézel (CNRS - IRMAR)

7 Travaux pratiques LEAN

Orateur: Patrick Massot