Axiom Math Completes First Computer-Verified Proof of the Classification of Finite Simple Groups

Details

Axiom Math announced the first complete computer-verified proof of the Classification of Finite Simple Groups (CFSG) in October 2026, formalizing the first-generation proof in the Lean proof assistant.
The project utilized a swarm of AI agents over 24 days to generate approximately 43.1 million lines of code, completing 108 milestones between October 2 and 25, 2026.
Formalization revealed 34 significant deviations from published literature, including a counterexample to a closure assertion in John Walter's Unbalanced Group Theorem (UGT) proof involving PSL₂(49) and PSL₂(7).
A new preservation theorem (Theorem 2.3) was developed and formalized to resolve the UGT gap, with a subsequent shortcut found within first-generation methods that bypasses the new theorem.
The proof builds on Mathlib and incorporates 1.2 million lines of code from the Qiuzhen-CFSG project, with an errata list available for the group theory community.
External advisors Richard Lyons and Ronald Solomon contributed to the resolution of the UGT issue and the curation of the errata list.

Key point