Les « assistants de preuve » sont des logiciels qui permettent d’entrer un énoncé de théorème et sa démonstration comme un programme, la compilation dudit programme garantissant que la démonstration proposée prouve effectivement l’énoncé donné. Initiés dans les années 60, ils font l’objet d’une grande activité scientifique depuis une trentaine d’années et ont permis de vérifier la correction d’énoncés tout à fait non triviaux.
Intéressé par ces développements, je me suis appliqué à démontrer la simplicité du groupe alterné au sein du logiciel Lean et de sa librairie mathématique mathlib.
Ce travail aurait pu n’être qu’un exercice de quelques semaines ; je raconterai la longue excursion mathématique qu’il m’a conduit à entreprendre, notablement accompagnés par Iwasawa et Jordan.
www.math.ens.psl.eu/evenement/simplicite/
*Documents associés*
Formalizing the proof of an intermediate-level algebra theorem-An experiment
arxiv.org/abs/2303.12404
Simplicité des groupes - une expérience incomplète de formalisation, Séminaire formath, IRIF, Université Paris Cité, 13 novembre 2023
webusers.imj-prg.fr/~antoine.chambert-loir/exposes/formath-20231113
Invariants birationnels en présence de formes-volume, SAGA, Université Paris-Saclay, 7 novembre 2023
What do we expect of a proof? --- The example of the simplicity of the alternating group., Quinzième colloque français de philosophie des mathématiques, 18-20 octobre 2023. Universités Paris 1 Panthéon-Sorbonne et Paris-Cité.
webusers.imj-prg.fr/~antoine.chambert-loir/exposes/philmath-20231019.pdf