Sites Inria

English version

Preuve informatique

Nathaly Mermet, Technoscope - 6/12/2012

La précision des ordinateurs au service des mathématiques

Laurence Rideau © Bernard Lachaud © Bernard Lachaud

Avec l’équipe Typical d’Inria Saclay - Ile-de-France, l’équipe Marelle de Sophia Antipolis a largement participé à l’aventure du projet Mathematical Components , sous la houlette de Georges Gonthier, dans le cadre du laboratoire commun Inria Microsoft Research.

Retour sur une expérience passionnante avec l’une des chercheuses de Marelle, Laurence Rideau.

Impliquée dès son démarrage en 2006 dans le projet Mathematical Components , aux côtés d'Yves Bertot - responsable de l’équipe Marelle - et de Laurent Théry, Laurence Rideau  retrace sa mise en place : « le projet a naturellement réuni des personnes qui connaissaient suffisamment l’outil Coq et étaient déjà familiarisées à la modélisation des mathématiques » . Ainsi la formalisation des mathématiques en Coq était elle au cœur de la démarche dès l’origine. 

Avec Coq, on arrive à une étape supplémentaire d’informatisation des mathématiques, à savoir que l’outil informatique aide, au-delà des calculs, à vérifier des raisonnements mathématiques

Feuille de route

« L’objectif du projet était très clair »  affirme Laurence «  il consistait à se donner les outils, les moyens techniques et informatiques, pour formaliser et démontrer des théorèmes de niveau maîtrise et même recherche en mathématiques » .  Dans le cadre d’une démonstration formelle le système ne fait pas la démonstration à la place du chercheur, mais vérifie en revanche que toutes les étapes sont cohérentes et que rien n’a été oublié. « Coq vérifie à chaque étape que les briques sont bonnes et s’imbriquent correctement » insiste t-elle, précisant que cet outil ne sert pas uniquement à faire des maths mais permet aussi de démontrer la correction de procédures ou d’algorithmes, y compris dans les programmes.

Preuve de concept

C’est au départ avec les théories mathématiques de base, arithmétique, algèbre, théorie élémentaire des groupes, que les choses ont été le plus travaillées. « Or si un développement mathématique est bien conçu, il peut être ré-utilisable pour d’autres démonstrations »  avance Laurence Rideau.

Quatre ans de travail ont été nécessaires pour aboutir à la mise en place de toutes les briques avant d’arriver à accéder au théorème final, dont la preuve a duré environ deux ans supplémentaires. « Le jour où l'on a inscrit le point final de la preuve a été un grand bonheur partagé »  confie t-elle, rappelant qu’elle avait au préalable épluché laborieusement 600 pages de mathématiques pures et que Georges Gonthier avait quant à lui assumé les choses les plus dures !  Dans les coulisses de cette réussite, un excellent travail collaboratif qui a permis d’avancer dans la formalisation mathématique à toutes les étapes. « Un ordinateur est borné, il n’a pas d’intuition mathématique ni de créativité en la matière. On doit donc lui fournir toutes les informations»  commente Laurence non sans humour. Moment de vérité : lorsque la démonstration est terminée en Coq, l’ordinateur recalcule tout et affiche le verdict! L’étape suivante sera de remettre le tout dans les mains des mathématiciens. Affaire à suivre…

Mots-clés : Mathematical components Equipe-projet MARELLE Coq Laboratoire commun Inria - Microsoft Research Inria research centre - Sophia Antipolis - Méditerranée

Haut de page

Suivez Inria