En 2004, G. Gonthier a achevé la preuve formelle du théorème de 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èmes 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.