Mathématiques en mouvement 2023 : Des preuves et des programmes
L'édition d'automne 2023 de Mathématiques en mouvement avait pour thème Des preuves et des programmes. Organisée sous la houlette de Hugo Herbelin (Inria, IRIF), elle a eu lieu le samedi 2 décembre 2023 à l'Institut Henri Poincaré (5 rue Pierre et Marie Curie, Paris 5e), amphithéâtre Hermite. Comme tous les ans, cette conférence était accessible aux étudiants et étudiantes, dès la licence.
Programme
-
14h00-14h10 : Accueil, introduction
-
14h10-14h40 : Et si les preuves mathématiques n’étaient autres que des programmes ?, par Hugo Herbelin (Inria, IRIF)
-
14h40-15h10 : Pourrait-on vérifier toutes les mathématiques sur ordinateur ?, par Riccardo Brasca (IMJ-PRG)
-
15h10-15h40 : Des programmes sans bugs grâce aux mathématiques formelles, par Jean-Marie Madiot (Inria)
-
15h40-16h00 : Pause café
-
16h00-16h30 : Démonstration automatique : l'exemple de Sniper, par Chantal Keller (LMF, Université Paris-Saclay)
-
16h30-17h00 : La fonction G de Hofstadter et au-delà ! Un exemple curieux mêlant calculs et preuves sur ordinateur, par Pierre Letouzey (IRIF, UPC, Inria)
-
17h00-18h00 : Table ronde
-
18h00-19h00 : Collation de clôture
Intervenant•e•s
RICCARDO BRASCA a effectué sa thèse en théorie de nombres à l'Université de Milan en 2012. Depuis 2013, il est maître de conférence à l'Université Paris Cité et membre de l'équipe Formes automorphes de l'Institut de Mathématiques de Jussieu-Paris Rive Gauche. Ses travaux de recherche portent sur le programme de Langlands et plus précisément sur la théorie des formes modulaires p-adiques. Depuis 2020, il s'intéresse beaucoup aux mathématiques formalisées et aux assistants de preuve, notamment à Lean et Mathlib, sa bibliothèque mathématique, dont il est un des responsables. Il a formalisé plusieurs résultats de théorie des nombres de niveau avancé et a participé au « Liquid Tensor Experiment », un projet pour lequel on a formalisé un théorème récent de Clau-sen et Scholze et qui représente un des succès les plus importants dans le domaine des mathématiques assistées par ordinateur.
HUGO HERBELIN est chercheur à l'Inria et spécialisé dans divers aspects de la correspondance entre preuves et programmes, essayant de croiser des concepts venant de la logique avec des concepts venant de la programmation, par exemple en étudiant comment les effets de bords de la programmation, tels que les exceptions, ou les affectations mémoire, peuvent être utiles pour calculer avec des axiomes logiques, tels que le raisonnement par contradiction ou l'axiome du choix. Cet intérêt se prolonge dans un croisement avec des concepts de la théorie des catégories ou de la géométrie, notamment dans le cadre de la théorie des types homotopiques (HoTT). Hugo Herbelin est aussi l'un des contributeurs à l'implémentation de l'assistant de preuve Coq.
CHANTAL KELLER est maîtresse de conférences de l'Université Paris-Saclay. Elle travaille sur les liens entre démonstration automatique et démonstration interactive, notamment dans l'assistant de preuves Coq.
PIERRE LETOUZEY est maître de conférences en informatique à l'Université Paris Cité, dans l'équipe commune Picube (UPC-IRIF, INRIA, CNRS). Ancien élève de l'ENS Ulm, il est agrégé de mathématiques et titulaire doctorat d'informatique effectué sous la direction de Christine Paulin. Il a longtemps participé au développement de l'assistant de preuves Coq, notamment de sa librairie standard et de son outil d'extraction vers OCaml. Ses thèmes de prédilection sont les confluences entre informatique, mathématiques et logique, les preuves formelles, la certification de code.
JEAN-MARIE MADIOT est chercheur à l'INRIA Paris dans l'équipe Cambium. Docteur en informatique de l'ENS Lyon et de l'Université de Bologne, ses domaines de recherche incluent la théorie de la concurrence, la preuve formelle de programmes, et la logique de séparation.
Vidéos et ressources
La FSMP avait eu la chance de rencontrer le mathématicien Vladimir Voevodsky (1966-2017), lauréat de la médaille Fields en 2002, qui nous racontait comment il avait délaissé ses premières amours mathématiques (la géométrie algébrique) pour se consacrer à la théorie des types, aux fondations univalentes, aux assistants de preuve.
Et si les preuves mathématiques n’étaient autres que des programmes ?, par Hugo Herbelin (Inria, IRIF)
L'idée s'est progressivement imposée au cours du 20e siècle que les preuves étaient aussi des programmes : par exemple une preuve de A⇒B peut être vue comme une fonction qui calcule une preuve de B à partir d'une preuve de A. Plus récemment, cette correspondance s'est élargie en direction de l'algèbre et de la géométrie, notamment avec la théorie des types homotopiques (HoTT) qui identifie l'égalité en logique avec la notion de chemin dans un espace. Nous donnerons quelques pistes dans la direction d'une fondation commune à tous ces domaines.
Pourrait-on vérifier toutes les mathématiques sur ordinateur ?, par Riccardo Brasca (IMJ-PRG)
Dans cet exposé, on montrera en pratique comment utiliser un assistant de preuve, en "expliquant" à l'ordinateur de simples résultats mathématiques. Puis on expliquera comment faire la même chose pour des théorèmes plus difficiles, à travers, en particulier, l'histoire du "Liquid Tensor Experiment", un projet dont le bût a été la formalisation des mathématiques de niveau recherche. On se concentrera sur les gains mathématiques d'un tel projet, en expliquant comment la formalisation peut aider les mathématiciens dans leur travail de chercheurs.
Des programmes sans bugs grâce aux mathématiques formelles, par Jean-Marie Madiot (Inria)
Écrire un programme sans erreur, c'est difficile, ça demande de penser à tous les cas possibles, même les plus bêtes. Peut-être qu'on pourrait utiliser un programme de test pour vérifier tous les cas ? Mais que faire s'il y a une infinité de cas ? Et si le programme de test a des erreurs ? Nous verrons comment raisonner mathématiquement sur les programmes permet de répondre à ces questions et comment l'ordinateur peut nous aider non seulement à tester mais aussi à prouver des programmes.
Démonstration automatique : l'exemple de Sniper, par Chantal Keller (LMF, Université Paris-Saclay)
Avoir des théorèmes dans l'ordinateur, c'est bien, mais laisser l'ordinateur démontrer ces théorèmes par lui-même, c'est pratique ! Oui, mais... est-ce toujours possible ? On donnera quelques notions permettant de comprendre les limites théoriques de la démonstration automatique, et on présentera quelques travaux permettant, en pratique, de résoudre malgré tout bien des problèmes.
La fonction G de Hofstadter et au-delà, un exemple curieux mêlant calculs et preuves sur ordinateur, par Pierre Letouzey (IRIF, UPC, Inria)
Dans son livre Gödel, Escher, Bach, Douglas Hofstadter définit une fonction récursive G ainsi : G(0)=0 puis G(n)=n-G(G(n-1)) pour tout entier n>0. Cette définition se généralise ensuite, donnant une curieuse famille de fonctions, nettement moins connues que G. Leur étude entremêle une étonnante variété de notions : arbres infinis, variantes de nombres de Fibonacci et systèmes de numération associés, mots morphiques, jolie fractale, etc. Plusieurs questions restent, des conjectures résistent encore. On verra comment le calcul est crucial ici pour se forger des intuitions (pas toujours exactes !) et comment des preuves sur ordinateur (ici en Coq) aident à se prémunir de tout type d'erreurs.
Quelques liens éventuels :
L'édition 2024 de Mathématiques en mouvement a eu lieu le samedi 16 novembre 2024 de 14h à 19h à l'IHP (11 rue Pierre et Marie Curie, Paris 5e). Organisée sous la houlette de Pierre-Antoine Guihéneuf (IMJ-PRG, SU) et Jérôme Buzzi (LMO, Univ. Paris-Saclay), c'était l'occasion d'aborder les systèmes dynamiques. La manifestation était placée sous le parrainage de la SMF. Elle bénéficiait également du partenariat du séminaire Mathematic Park.
L'édition du printemps 2023 a eu lieu le samedi 13 mai 2023 à l'IHP sous le titre À l'eau les maths !. Sous la houlette de Jacques Saint-Marie (Inria), on a exploré les rôle des maths dans la résolution de diverses problématiques liées à l'eau.
L'édition 2022 de Mathématiques en mouvement a eu lieu le samedi 11 juin 2022 à l'IHP, sous la houlette de Rida Laraki, directeur de recherche CNRS au LAMSADE et en partenariat avec Math Park.