Forum de mathématiques - Bibm@th.net

Barbichu

Membre actif

Inscription : 15-12-2007

Messages : 405

La formalisation du Théorème de Feit-Thompson en Coq

Chers Bibmatheux,

pour vous changer de vos (il-)lectures récentes à propos de la conjecture de Syracuse. J'ai l'honneur de vous mettre sous la dent la nouvelle de l'achèvement récent de quelque chose que je considère comme extraordinaire.
http://www.msr-inria.inria.fr/events-ne … ved-in-coq
Il s'agit d'une formalisation complète, dans l'assistant à la preuve Coq, du théorème de Feit-Thompson, stipulant que tout groupe d'ordre impair est résoluble.

Pour faire court, la preuve originale (mais aussi la preuve révisée) de ce théorème tient sur plusieurs centaines de pages et repose sur des prérequis en théorie des groupes, en théorie de Galois et en théorie des caractères, ce qui fait que seuls quelques spécialistes sur cette planète peuvent affirmer l'avoir lue et comprise dans son intégralité (et je n'en fais pas partie ;)). L'assistant à la preuve Coq est un outil permettant de formuler des définitions, des théorèmes et des démonstrations mathématiques et de vérifier ces dernières mécaniquement. À l'issue de 6 ans d'efforts, une équipe de chercheurs menée par Georges Gonthier (Microsoft Research Cambridge), au sein du centre commun Inria-MSR, a abouti à une formalisation complète et certifiée du-dit théorème, ce qui non seulement apporte la certitude que le théorème est vrai (même si ce fait était déjà bien accepté dans la communauté mathématique), mais montre aussi que la preuve formelle a de beaux jours devant elle.

Par ailleurs, je pointe les intéressés vers une preuve formelle, encore inachevée à ce jour, de la conjecture de Kepler (dans un autre assistant de preuve : HOL Light) : http://code.google.com/p/flyspeck/

Formellement vôtre,