Sites Inria

English version

Preuve informatique

Nathaly Mermet - 22/11/2012

La preuve mathématique par informatique !

© Photo Bernard Lachaud

Une démonstration formelle complète, certifiée par le logiciel Coq, a été annoncée en septembre par Georges Gonthier et son équipe du laboratoire commun Inria-Microsoft Research.

Ces travaux rendent artificielle l’opposition entre informatique et mathématiques, le dénominateur commun étant la logique. Parmi les "compagnons de route" de Georges Gonthier, deux jeunes chercheurs se réjouissent d’avoir participé à l’aventure et "grandi" avec le projet Mathematical Components (MathComp). Témoignages…

Vous sentez-vous privilégié.e d’avoir contribué au succès des derniers travaux de Georges Gonthier ?

© Inria / Photo Kaksonen

Assia Mahboubi, chargée de recherche chez Inria depuis 2007 et membre de l'équipe MathComp depuis 2006.
Georges Gonthier jouissait déjà d'une grande notoriété avant le succès de ce projet autour de la preuve formelle du théorème de Feit-Thompson. Ses contributions dans le domaine de l'informatique sont multiples, mais sa vérification du théorème des quatre couleurs, en collaboration avec Benjamin Werner (Inria) a jeté un coup de projecteur sur notre thématique.


© Photo Bernard Lachaud

Enrico Tassi,  chargé de recherche chez Inria depuis septembre 2012 après un postdoc sur le projet (terminé fin 2011). A travaillé sur le projet dans le cadre de son doctorat à Bologne (Italie) pendant six mois (fin 2006/début 2007).
L’idée de faire des maths avec un ordinateur, et avec pour but de vérifier la preuve, m’a beaucoup plu. L’étude et le développement d’outils comme Coq ont effectivement été au cœur de mes études en master et thèse. Le laboratoire commun Inria-Microsoft Research venait d’être créé et c’était une excellente opportunité pour venir travailler avec les meilleurs experts du domaine.


Que représente pour vous ce domaine de recherche et quel est le fond de votre motivation ?

Assia Mahboubi  : Il s'agit d'une activité assez transverse qui questionne la notion philosophique de vérité mathématique aussi bien qu'elle peut apporter des réponses aux besoins modernes de sécurité informatique. Il est extrêmement difficile d'avoir une confiance absolue dans la preuve d'un théorème. Nous essayons de transcrire les énoncés mathématiques et leur démonstration dans le langage très simple et parfaitement codifié qu'est la logique, pour qu'un ordinateur puisse nous aider à les vérifier. Cette recherche a de multiples aspects, et pose de nombreuses questions : qu'est-ce qu'une preuve mathématique? Qu'est-ce qu'un programme ? Qu'est-ce que la logique ?

Enrico Tassi  : Quand un argument est-il valide? Ce problème a été étudié pendant des centaines d’années, depuis les philosophes comme Aristote, jusqu'aux mathématiciens tels Hilbert et Gödel. Notre recherche essaie de répondre positivement aux questions suivantes : les ordinateurs peuvent-ils assister l’Homme à formuler des arguments complexes et originaux sans induire d’erreur ?  Peuvent-ils aider les scientifiques face à la complexité croissante des théories mathématiques qu’ils développent ?

Comment vous projetez-vous à la lumière du projet aujourd’hui abouti ?

Assia Mahboubi  : L’idée de s'aider d'un ordinateur pour faire des preuves n'est pas nouvelle : c'est un domaine d’investigation chez Inria depuis plusieurs décennies. La nouveauté avec ce succès c'est que l'approche passe à l'échelle pour de "grosses preuves" et de "grands théorèmes". De nombreux domaines utilisant des programmes informatiques critiques (aéronautique, cryptographie...) bénéficient déjà des applications de ce champ de recherche. Mais maintenant, nous pensons qu'il peut aussi intéresser un spectre plus large de scientifiques, incluant des mathématiciens n'utilisant jusqu'à présent que papier et tableau noir.

Enrico Tassi  : Le projet terminé montre qu’on pouvait vérifier des théories mathématiques complexes avec un ordinateur. Mais le travail n'est pas fini car il faut encore rendre cette technologie utilisable par tous les scientifiques, et pas seulement par les experts de preuve formelle comme nous.

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

Haut de page

Suivez Inria