Sites Inria

English version

Preuve informatique

Françoise Breton - 22/11/2012

Un grand succès pour la preuve informatique

© Inria / Photo Kaksonen

Six 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.

Réussir à faire la preuve que cette démonstration est correcte et complète est donc une entreprise de taille que Georges Gonthier et son équipe, Laurent Théry, Laurence Rideau, Assia Mahboubi, Enrico Tassi et bien d'autres, ont mis six ans à achever. Il s’agit en effet de faire "comprendre" la démonstration à l’ordinateur et pour cela il est nécessaire de lui "enseigner" toutes les mathématiques dont il aura besoin : théorèmes, démonstrations, etc., mais aussi la manière de s’en servir, une compétence qui transparaît uniquement dans les notations présentes dans la partie des livres de cours consacrée aux exercices. La principale difficulté résidait dans la codification de cette partie opérationnelle. Les chercheurs ont été aidés en cela par leur formation d’informaticiens rompus à l’utilisation de langages permettant de décrire les procédés utilisés, et grâce aux règles cachées que les chercheurs ont identifiées derrières les notations mathématiques. Une ligne de mathématique peut ainsi correspondre à un contenu implicite de deux pages !

Au final : une bibliothèque informatique de mathématiques imposante et un enrichissement de la boîte à outils Coq et de son environnement. Les chercheurs ont ainsi développé un langage au-dessus de Coq qui permet de décrire des démonstrations compliquées. La preuve a également permis de tester les capacités du logiciel de certification. Il faut 1h40 pour compiler les 170 000 lignes de la démonstration.

Le théorème qui a fondé l’algèbre moderne

Le théorème de Feit et Thompson est la pierre angulaire de la théorie des groupes moderne, et donc de la classification des groupes simples, qui est elle-même la pierre angulaire de l’algèbre moderne. La théorie des groupes étudie les opérations réversibles, ce qui devient vite compliqué lorsque le nombre de dimensions augmente. Elle trouve des applications dans des domaines très variés dont la plus ancienne historiquement est la cristallographie : la théorie des groupes permet d’interpréter les interférences provoquées par l’illumination d’un cristal par les rayons X afin d’en déduire la structure du cristal. Dans le domaine grand public, la théorie des groupes est à l’origine de casse-tête comme le rubik’s cube pour lequel chaque manipulation est réversible.
 Les recherches mathématiques sur les groupes se sont développées au milieu du 20e siècle lorsque l’on s’est aperçu qu’ils étaient très utiles. Les mathématiciens ont voulu étudier leurs propriétés en utilisant une méthode consistant à factoriser les groupes, c’est-à-dire à les décomposer en facteurs de groupes élémentaires (dits simples) à la manière des entiers décomposés en facteurs de nombres premiers (30=2*3*5). Cette méthode permet de restreindre l’analyse des propriétés à celle des groupes simples, qui peut se faire systématiquement grâce à une classification énumérant toutes les formes possibles de groupes simples (3 types génériques et 26 exceptions). En 1955 Brauer avait montré que l’on pouvait classifier un groupe en étudiant ses involutions, mais cette technique ne fonctionne pas pour les groupes d’ordre impair. C’est là qu’intervient le travail de Feit et Thompson qui, en démontrant que tous les groupes impairs sont résolubles, a ouvert la voie à l’étude des groupes pairs. Ils ont également fourni des méthodes totalement nouvelles et sont à l’origine d’un changement de perspective dans les mathématiques. La publication du théorème en 1963 prenait en effet la forme d’un article comptant 250 pages, ce qui était inédit à une époque où les démonstrations mathématiques élégantes les plus longues ne dépassaient pas 20 pages. De quoi alimenter des doutes sur le sérieux du travail ! La classification des groupes simples d’ordre pair, qui s’est poursuivie jusqu’en 2003, fait pour sa part 10 000 pages…

Mots-clés : Inria Saclay - Île-de-France Georges Gonthier Preuve Laboratoire commun Inria - Microsoft Research Théorème Feit et Thompson Inria Sophia Antipolis - Méditerranée

Haut de page

Suivez Inria