Séminaire réflexions : démonstration, rigueur et formalisation
Le « Séminaire réflexions », est commun aux Archives Henri Poincaré, à l’Institut Élie Cartan de Lorraine et au Loria et a pour but est de proposer des exposés d’intérêt général.
Alexandre Afgoustidis (IECL), Alain Genestier (IECL) et Yacin Hamami (AHP) organisent cette année autour du thème « Démonstration, rigueur et formalisation. »
Ces dernières années, les preuves assistées par ordinateur ont suscité un engouement certain dans la communauté mathématique. Nous parlons ici des outils de vérification pour les preuves les plus traditionnelles (donc pas, ou très peu, d’« apprentissage artificiel » ).
Comment ces outils fonctionnent-ils et comment les utiliser ? Quels sont leurs atouts, leurs limites ? Quelles sont leurs répercussions sur la recherche en mathématiques, et sur l’idée que nous nous faisons des notions de rigueur et de démonstration ?
Ces questions, et d’autres, seront abordés avec exposés, tables rondes, tutoriels et groupes de travail. Le séminaire se réunira 6 fois au premier semestre 2026.
L’automatisation dans les assistants de preuve.
L’exposé sera suivi d’un groupe de travail « Math en LEAN » pour démarrer des projets de formalisation avec les conseils d’utilisateurs expérimentés d’assistants de preuve..
