Séminaire Des mathématiques

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. […]