Le Colloquium

Les assistants de preuves sont des logiciels permettant de rédiger des énoncés mathématiques et leur démonstration, la compilation du tout garantissant (modulo d'infimes détails) la correction de l'ensemble. Après avoir été surtout promu par la communauté informatique, ils font l'objet d'un engouement croissant chez les mathématicien·nes.

Il y a quelques mois, j'ai formalisé au sein du logiciel Lean/mathlib une démonstration d'un théorème classique, élémentaire, de théorie des groupes : la simplicité du groupe alterné sur au moins 5 lettres, via un critère d'Iwasawa généralement utilisé pour démontrer la simplicité des groupes géométriques.

Je présenterai ce travail, son contexte, et quelques perspectives. (Aucune familiarité avec les assistants de preuve n'est requise.)