Avancée dans la preuve informatique

6 ans après la démonstration par ordinateur du théorème des quatre couleurs, Georges Gonthier et son équipe réussissent la démonstration, autrement plus complexe, du théorème de Feit et Thompson, un théorème central pour la théorie des groupes et leur classification. Grand pas pour les mathématiques, qui s’appuient de plus en plus sur la preuve par ordinateur, c’est surtout une réussite pour l’informatique qui montre là sa capacité à déployer des outils et des techniques de qualité pour codifier les mathématiques.

Après la validation du théorème des quatre couleurs par le logiciel de certification Coq en 2005, c’est au tour du théorème de Feit et Thompson de passer dans la moulinette de la preuve informatique. La difficulté était cependant incomparable car, si le théorème des quatre couleurs n’utilise que des mathématiques combinatoires élémentaires, le théorème de Feit et Thompson s’appuie sur des mathématiques embrassant, grosso modo, le programme jusqu’à la licence ! Il est également plus long, avec ses 250 pages de démonstration, et les enjeux autrement importants, avec des applications dans de nombreux domaines scientifiques modernes, de la mécanique quantique à la cryptographie, en passant par la cristallographie.

La suite de l'article ICI et les témoignages des membres de l'équipe ICI .