Events

23 November 2007

Assia Mabhoubi gives seminar at INRIA Rocquencourt

Preuve formelle à grande échelle et réflexion à petite échelle
Assia Mahboubi

I N R I A – Rocquencourt
Amphi Turing du bâtiment 1

Vendredi 23 novembre, 10h30

En 2004, G. Gonthier a achevé la preuve formelle du théorèmes des quatre couleurs dans l’assistant à la preuve Coq.

L’une des clefs de cette réussite est une utilisation intensive de techniques dites de “réflexion à petite échelle”, soutenues par une extension du langage de tactiques de Coq. Cette extension, ainsi qu’une partie des bibliothèques développées pour la preuve, sont actuellement utilisées comme point de départ pour le projet de formalisation d’une somme substantielle de théorie des groupes finis, dans l’équipe Composants Mathématiques du centre commun INRIA Microsoft Research.

Il s’agit cette fois de construire une preuve formelle du théorème de Feit-Thompson (1963), qui constitue un passage a l’échelle significatif pour les contributions issues de la preuve du théorème des quatre couleurs.

Le but de cette expérience est de comprendre comment mener à bien le développement de bibliothèques de mathématiques formalisées, réutilisables et combinables. Nous tenterons d’abord de dégager les difficultés que présente la réalisation de telles bibliothèques, puis de présenter les techniques qui se dégagent de la preuve du théorème des quatre couleurs, et des travaux en cours sur la théorie des groupes et en particulier le langage de tactiques ssreflect.