Sites Inria

English version

Preuve informatique

Françoise Breton - 22/11/2012

Georges Gonthier : Notre diagramme de travail ressemblait à un plan de guerre napoléonienne !

Georges Gonthier, laboratoire commun Microsoft Research-Inria © Laboratoire commun Inria-Microsoft Research

Six années se sont écoulées entre le début du projet et la fin de la preuve du théorème de Feit et Thompson réalisée le 20 septembre 2012. Récit d’une aventure moderne.

Entretien avec Georges Gonthier, laboratoire commun Microsoft Research-Inria.

Quel était l’objectif du projet ?

Il s’agissait de traduire le sens de l’énoncé mathématique sous une forme compréhensible pour l’ordinateur afin que ce dernier puisse déterminer si la démonstration est correcte et complète. La démonstration est en fait le but ultime qui permet de tester tous les développements réalisés en amont et nécessaires pour la réaliser. En effet, cette démonstration s’appuie sur de nombreux domaines mathématiques : l'algèbre linéaire, la géométrie, la théorie des nombres, la théorie de Galois, des corps finis, etc. Il fallait développer les bibliothèques de mathématiques nécessaires pour réaliser toutes les étapes de la démonstration.
Nous avons ainsi passé les trois premières années à codifier les mathématiques plus simples, puis une année à réaliser une première moitié de la démonstration qui reposait sur ces types de mathématiques. Une autre année a été nécessaire pour développer les outils pour une autre branche des mathématiques, puis une dernière année pour la deuxième partie de la démonstration.

Comment a été organisé le travail sur ces six années ?

Une dizaine de chercheurs et de postdoctorants ont contribué à ce travail à des degrés différents et pendant des périodes de temps différentes. En tant que coordinateur j’étais à temps complet sur le problème. Le travail était nécessairement réparti du fait de la dispersion géographique des participants à Cambridge, Inria Saclay et Inria Sophia Antipolis. Mais plusieurs chercheurs pouvaient travailler sur le même problème sur un site donné. Pour le dernier bout de preuve le 20 septembre, tout le monde a mis la main à la pâte !

Aviez-vous prévu que ce travail prenne autant d’années ?

J’avais déjà acquis une expérience avec la démonstration du théorème des quatre couleurs. Je savais que la mise en place des fondements est longue avant de voir ensuite effectivement le travail avancer : il faut comprendre comment construire les bibliothèques avant de les réaliser et, but ultime, de les tester par cette preuve. J’avais prévu que l’ensemble prendrait cinq à six ans. Donc pas de surprise de ce côté ! Pour mes collègues en revanche c’était différent. Lorsque j’ai griffonné il y a six ans un diagramme représentant toutes les parties à développer et leurs interconnexions, mon auditoire a conclu au plan d’une guerre napoléonienne ! Le 20 septembre j’ai reçu une photo de moi accoutré d’un bicorne !

Avez-vous eu des surprises au cours de ce travail ?

Nous avons eu quelques bonnes surprises, notamment sur la manière d’écrire les bibliothèques afin d’être en mesure de les assembler de manière flexible. C’était un problème de fond que nous avons abordé en nous appuyant sur le même principe que pour réaliser les composants logiciels facilement connectables entre eux : en ajoutant une partie de code stipulant comment se combiner avec d’autres logiciels. Et là, j’ai découvert que l’on pouvait utiliser le même mécanisme que pour l’interprétation des annotations mathématiques et que Coq disposait des outils nécessaires. Nous avons également identifié quelques erreurs de transcription sans conséquences dans la démonstration grâce au programme.

Quel est l’impact de ce travail ?

Le fait que l’on arrive à faire par ordinateur un problème réputé difficile montre qu’il y a des progrès réalisés dans la qualité des outils et des techniques mis en œuvre dans ce travail de codification des mathématiques. C’est un peu tôt pour juger de l’impact de cette démonstration. Mais nos résultats ont été rendus disponibles au fur et à mesure de leur élaboration et les bibliothèques développées ont déjà été reprises : aujourd’hui un nombre important de publications utilise Coq et notre bibliothèque. Il nous faut maintenant mettre l’accent sur la diffusion de nos résultats qui a été un peu mise de côté durant ces années.

Et y a-t-il une suite prévue pour ces travaux ?

Nous devons aujourd’hui tirer les leçons de l’expérience réalisée pour préparer des outils pour la suite et prendre le temps de la réflexion. La notoriété aidant, nous avons déjà reçu des suggestions de problèmes. La suite naturelle serait le théorème de classification complet mais c’est une entreprise qui dépasse de loin les moyens humains du labo commun. Il faudrait y associer les labos de mathématiques du monde entier ! J’ai aussi quelques idées de mon côté mais rien n’est encore décidé.

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

Haut de page

Suivez Inria