Feit–Thompson odd-order theorem

feit_thompson

Submitter: Kim Morrison.

Notes: Every finite group of odd order is solvable. W. Feit and J. G. Thompson, Pacific J. Math. 13 (1963), 775-1029. A 255-page paper that opened the path to the Classification of Finite Simple Groups; Thompson received the Fields Medal in 1970 in part for this work. Coq formalization by Gonthier et al. 2012 (~170 000 lines); no Lean port. Stated with zero new definitions on top of mathlib (IsSolvable, Odd, Nat.card, Group, Finite). Honorable-mention entry on Freek Wiedijk's 'Formalizing 100 Theorems' page (alongside the Classification of Finite Simple Groups itself).

Source: W. Feit and J. G. Thompson, Solvability of groups of odd order, Pacific J. Math. 13 (1963), 775-1029. Coq formalization: G. Gonthier et al., A Machine-Checked Proof of the Odd Order Theorem, ITP 2013 (https://hal.inria.fr/hal-00816699). Listed as a named honorable mention on https://www.cs.ru.nl/~freek/100/.

Informal solution: The proof proceeds by contradiction: assume G is a minimal counterexample, a non-solvable group of minimal odd order. (i) Generic case: by Hall-Wielandt and the Feit-Hall theorem on solvable signalizer functors, G has a unique conjugacy class of maximal subgroups containing every Sylow normalizer; rule out via character-theoretic identities (Suzuki's Brauer table machinery). (ii) Uniqueness case: G has a single 'large' maximal subgroup M whose structure is heavily constrained; case analysis on |M|/|G| and the action of M on its Frobenius-like complements gives the contradiction. (iii) The 'CN' (centralizer-normalizer) and 'CIT' (centralizer-of-involution-trivial) case analyses use the Frobenius theorem on Frobenius groups (whose only known proof uses character theory) to constrain centralizer structure. The whole argument is organized around the dichotomy 'large' vs 'small' Sylow 2-subgroups (or rather Sylow 2-substructures, since |G| is odd: there are none, so the dichotomy is about Sylow p for the smallest p dividing |G|).

theorem declaration uses `sorry`feit_thompson {G : Type*} [Group G] [Finite G]
    (_h : Odd (Nat.card G)) : IsSolvable G := byG:Type u_1inst✝¹:Group Ginst✝:Finite G_h:Odd (Nat.card G)⊢ IsSolvable G
  sorryAll goals completed! 🐙

Solved by

Not yet solved.