Le Théorème de Feit et Thompson.
En théorie des groupes, le théorème de Feit et Thompson ou théorème de l'ordre impair, dit que :
- Tout groupe fini d'ordre impair est résoluble.
Ce qui équivaut à dire que :
- Tout groupe simple fini non commutatif est d'ordre pair.
Explications.
- Pour les notions de groupes :
Groupes, sous-groupe, ordre, groupe distingué, quotient ... - Un groupe fini d'ordre impair est un groupe G de cardinal impair.
- Un groupe fini G est dit résoluble
s'il possède une suite ( Gi )0 ≤ i ≤ r , finie décroissante de sous-groupes telle que :
- G0 = G ⊃ ... ⊃ Gr = {e} ;
- G i+1 soit un sous-groupe distingué de Gi pour 0 ≤ i ≤ r - 1 ;
- G i / G i+1 soit commutatif pour 0 ≤ i ≤ r - 1.
Applications.
Ce théorème et plus généralement la théorie des groupes, dont la figure historique mythique est le célèbre Évariste Galois, trouve des applications dans des domaines très variés dont la plus ancienne est la cristallographie.
La théorie des groupes permet d'interpréter les interférences provoquées par l'illumination d'un cristal par les rayons X afin d'en déduire la structure du cristal.
La théorie des groupes est aussi à l'origine du fameux rubik's cube pour lequel chaque manipulation est réversible.
Histoire.
Ce théorème, conjecturé en 1911 par William Burnside, fut démontré en 1963 par Walter Feit et John Griggs Thompson, dans une preuve de plus de 250 pages, ce qui était pour l'époque un évènement car la plupart des démonstrations ne dépassaient pas les 20 pages.
Le théorème lui-même et bon nombre de techniques que Feit et Thompson ont utilisé dans sa démonstration jouèrent un rôle important dans la classification des groupes.
En septembre 2012, une équipe jointe d'INRIA-Microsoft Research a annoncé 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 véritable exploit que d'arriver à décrire les lemmes, propositions et théorèmes multiples utilisés dans la démonstration globale et de coder des liaisons logiques.
Le code utilisé comporte d'ailleurs 170 000 lignes et il faut 1h40 pour le compiler.
Remarque : Le premier succès de ce type était la preuve de la validité de la démonstration du théorème des quatre couleurs.
Références.
- Annonce de l'INRIA.
- [Esco] : Jean-Pierre ESCOFIER, Théorie de Gallois, Masson, Paris, 1997.
