nLab
Feit-Thompson theorem

Statement

Theorem

Every finite group of odd order is a solvable group.

This is due to (Feit-Thompson 1962).

A fully formalized proof in Coq has been announced in (INRIA 2012)

References

• Walter Feit, John Thompson, A solvability criterion for finite groups and some consequences, Proc. Nat. Acad. Sci. 48 (6): 968–970, (JSTOR)

• INRIA, Feit-Thompson theorem has been totally checked in Coq