Assia MAHBOUBI - Vérifier des preuves mathématiques avec un ordinateur

Les assistants à la preuve sont une famille relativement méconnue de logiciels pour faire des mathématiques avec un ordinateur. Ils permettent à leurs utilisateurs de vérifier avec la plus grande certitude possible la validité des démonstrations qu’ils ont préalablement décrites à la machine. Le premier grand succès de cette approche de la vérification mathématique date sans doute de 2005, lorsque la preuve du théorème des quatre couleurs a été formalisée complètement à l’aide d’un tel assistant à la preuve. La seule preuve de ce résultat connue à ce jour mélange des arguments de combinatoire avec des calculs importants, impossible à effectuer à la main, qui confèrent pour certains un statut controversé à la démonstration. En septembre 2012, une preuve du théorème de l’ordre impair (Feit-Thompson, 1963), pierre angulaire de la classification des groupes simples finis, a également été vérifiée par un assistant à la preuve. Cette preuve ne repose aucunement sur des arguments calculatoires. Il s’agit d’une combinaison sophistiquée de théories algébriques, et la preuve de Feit et Thompson fut en son temps l’une les plus longues de la littérature mathématique.