Séminaire de mathématiques accessibles

Orateur : Filippo A. E. Nuccio (ICJ-UJM) : "Ordino ergo sum"

Séminaire de Mathématiques Accessibles à l'Institut Camille Jordan :

Des exposés d'1 heure, au rythme d'un exposé par mois, accessibles à un public plus large que les séminaires spécialisés traditionnels.

Public visé :
- au moins tout enseignant chercheur en maths pures et appliquées.
- souvent enseignants chercheurs d'autres disciplines connexes, étudiants...
- ponctuellement, public plus large (lycéens...).

Le "séminaire de mathématiques accessibles" fait sa rentrée Lundi 27 septembre à 16:00:

Orateur: Filippo A. E. Nuccio (ICJ-UJM)

Lieu: Salle 112 de la faculté des sciences de Saint-Etienne (Campus Métare)

Titre: Ordino ergo sum

Résumé: 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é.