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.