Formalization of the Classification of Finite Simple Groups

Work in progress.

Finished Theorems

(a) The Odd Order Theorem (Feit–Thompson)

Every finite group of odd order is solvable.

(b) The Strongly Embedded Subgroup Theorem (Bender–Suzuki)

If $X$ is a finite simple group containing a strongly embedded subgroup, then $X \cong L_2(2^n)$, ${}^2B_2(2^{n/2})$, or $U_3(2^n)$ for some $n\ge 2$.

(c) Gorenstein–Walter theorem

The classification of finite groups with a dihedral Sylow 2-subgroup.

Auditable statements

lake exe cache get
lake build lean4export
lake exe comparator comparator/config.json

Publications

• FormaTheoria: Constructing Large-Scale Lean Theories from Mathematical Literature. Tianjiao Nie, Ao Zhang, Yusen Tang, Damiano Testa, Shing-Tung Yau, Peng Li, Yuan Zhou. arXiv:2608.10894.