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