Sélectionnez votre langue

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.

 affiche MEM Automne 2023

 Cliquez ici pour télécharger l'affiche.

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

 

Deux interviews en lien avec le sujet...

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... Une interview à découvrir ici : https://www.youtube.com/watch?v=b6SgBCWPd6Y

Retrouvez également l'interview de Pierre-Louis Curien.

 

Résumés, présentations et vidéos des exposés

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.
Cliquez ici pour retrouver la présentation de l'exposé.

 

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.
Cliquez ici pour retrouver la présentation de l'exposé.

 

 

 

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.
Cliquez ici pour retrouver la présentation de l'exposé.

 

 
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.
Cliquez ici pour retrouver la présentation de l'exposé.

 

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.
Cliquez ici pour retrouver la présentation de l'exposé.

 

Quelques liens éventuels : 
- Une page généraliste pour commencer sur G (puis H, etc) : 
  https://fr.wikipedia.org/wiki/Suite_de_Hofstadter
 
- Mon code (et un ancien article) : https://github.com/letouzey/hofstadter_g

 Table ronde

 

 

Orateurs oratrice MEM PP1