Salle des séminaires C 112 (ICJ STE Campus Métare)
Salle des séminaires C 112
ICJ STE Campus Métare
ICJ STE 23 rue du Docteur Paul Michelon
42023 Saint-Étienne Cedex 2
Description
Fin 2020, un allemand nommé Peter Scholze, mathématicien d'assez bon niveau, tomba en proie d'un doute commun à nombre de ses collègues: "je viens de pondre une démonstration sur une feuille, elle m'a l'air plutôt solide, j'en suis même sûr au 99,9%: sera-t-elle vraiment correcte?". L'énoncé (probablement) démontré portait sur une propriété sophistiquée de certains espaces de Banach qui venait juste d'être introduite: où trouver de braves gens prêts à étudier, vérifier, décortiquer, éplucher, et enfin certifier que tout allait pour le mieux?
Dans cet exposé je parlerai un peu de ce qu'est un assistant de preuve, un logiciel conçu pour digérer des preuves d'énoncés mathématiques, et en restituer une validation formelle — ou un déni impitoyable. Je montrerai des exemples de raisonnement qu'on peut faire faire à un ordinateur et des notions mathématiques qu'on a déjà formalisées, en les traduisant en lignes de code pour que l'ordinateur puisse avancer tout seul. Finalement, je relaterai de comment un assistant de preuve entendit le signal de détresse banachique de Scholze et comment se passa le sauvetage.
Aucun prérequis d'informatique théorique, d'analyse fonctionnelle, d'espaces perfectoïdes (ou d'autres scholzeries) n'est nécessaire pour suivre l'exposé.