Magazine Science

Avancée dans la preuve informatique

Publié le 02 décembre 2012 par Olivier Leguay

1354470170_blue_monster_happy.png6 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 .


Retour à La Une de Logo Paperblog

A propos de l’auteur


Olivier Leguay 1825 partages Voir son profil
Voir son blog

l'auteur n'a pas encore renseigné son compte l'auteur n'a pas encore renseigné son compte