Actualités

Preuve formelle du théorème de Feit-Thompson

Le 15 octobre 2012

Le théorème de Feit et Thompson est une propriété portant sur les groupes finis qui est aussi simple à énoncer que difficile à démontrer : tout groupe fini d’ordre impair est résoluble.

Conjecturé en 1911 par Burnside, démontré par Feit et Thompson en 1963, ce théorème a nécessité l’introduction de méthodes innovantes et a joué un rôle décisif dans la colossale classification des groupes finis simples. La preuve originale occupe 250 pages ; elle a été un peu simplifiée mais pas considérablement raccourcie depuis.

Une équipe jointe d’INRIA-Microsoft Research a annoncé fin septembre la certification de la preuve par le logiciel Coq — une preuve que la preuve est correcte. Même si personne ne doutait du résultat mathématique, il s’agit d’un tour de force informatique qui montre la vigueur du domaine de la preuve assistée par ordinateur. Le premier succès de ce type était la preuve de la validité de la démonstration du théorème des quatre couleurs.

Pour mesurer le travail que cette vérification représente, on peut jeter un œil aux chiffres avancés par un des membres du projet, Laurent Théry :

Number of lines ∼ 170 000
Number of definitions ∼ 4 200
Number of theorems ∼ 15 000
Fun ∼ enormous !

Tout ceci donne aussi, en creux, une idée de la complexité de la preuve et de la profondeur de la vision de Feit et Thompson...

Une présentation du projet en anglais : Theorem Proof Gains Acclaim

Quelques mots sur les groupes

Les groupes ne sont pas des objets mathématiques aussi populaires que les fractals ou les ondelettes (même si une recherche sur ce site donne 277 articles...). Pourtant, Alexandre Grothendieck « n’hésite pas à parler de l’invention du zéro et de l’idée de groupe comme deux des plus grandes inventions mathématiques de tous les temps », comme le note Yves André dans un article sur Évariste Galois. Le concept de groupe traduit l’idée de symétrie, de transformation. Un groupe fini est donc constitué d’un nombre fini de « symétries ».

Le théorème de Feit-Thompson a ceci de remarquable qu’il met en relation une hypothèse de type « géométrique » (portant sur le cardinal du groupe) et une conclusion de type « algébrique » (la résolubilité est une propriété de structure qui intervient dans l’étude des « symétries » d’une équation que permet son groupe de Galois). Et la méthode repose sur la théorie des représentations.

[Brève corrigée le 12/11/2012 : la version précédente parlait de façon incorrecte de « preuve automatique » ; le lien ci-dessus n’était pas le lien officiel ; ajout du lien vers l’article de présentation en anglais.]

L'annonce du résultat sur le site d'INRIA

Partager cette actualité

La tribune des mathématiciens

Suivre IDM