Journées mathématiques X-UPS 2026 : Vérification formelle de preuves
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.
La page web de ces journées, qui sera complétée avec noms des conférenciers, titres, résumés et textes des conférences.
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
Les Journées mathématiques X-UPS bénéficient du soutien de la fondation mathématique Jacques Hadamard (FMJH).
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.