Axiom Math Completes First Full Lean Computer Formalization of the 15,000 Page Classification of Finite Simple Groups
The largest math proof in human history is now computer-verified. Today, Axiom announces a complete Lean auto-formalization of the Classification of Finite Simple Groups, the "periodic table of symmetry." About 15,000 pages, built by over 100 mathematicians across generations.
Context
Compressing the longest proof in mathematical history into 43.1 million lines of machine verified Lean code in just 24 days while uncovering 34 errors in the published record demonstrates that multi agent swarms can audit and repair human mathematics at unprecedented scale.
Known as the Enormous Theorem, the Classification of Finite Simple Groups establishes that every finite simple group belongs to three infinite families or 26 sporadic groups including the Monster group, with the original proof spanning roughly 15,000 pages across more than 500 papers written by over 100 mathematicians. Because of its vast dispersion across decades of literature, gaps such as the quasithin case took decades to close and the multi volume second generation revision remains incomplete.
Deep dive
On October 27, Axiom Math announced the first complete computer verified formalization of the Classification of Finite Simple Groups in the Lean proof assistant. Starting on October 1 with an internal proof map that divided the first generation classification proof into 108 milestones and roughly 380 tasks, Axiom engineers and mathematicians directed swarms of over 150 concurrent AxiomProver AI agents across 24 days, generating 2.0 million commits, 3,579 verified sub milestones, and approximately 43.1 million lines of Lean code.
To prevent Lean build times from bottlenecking the swarm, Axiom built a distributed build cache and externalized heavy finite group calculations into independently checkable certificates. By October 10, the agent swarm proved that the Monster group is simple via the 196,884 dimensional Griess algebra, and on October 13 engineers ran an automated replanning pass that decomposed remaining coarse milestones into fine grained theorems.
Translating 15,000 pages of dense prose into Lean exposed numerous typographical errors, dropped hypotheses, and 34 substantive deviations from the published mathematical record. In Michael Aschbacher and Stephen Smith's quasithin volumes, agents discovered a counterexample involving SL2(5) where a lemma asserted two quantities were equal when one was 1 and the other was 2, requiring a revised case split. More dramatically, while formalizing John Walter's 1986 memoir on the Unbalanced Group Theorem, agents found an explicit counterexample using the field involution of PSL2(49) whose centralizer PGL2(7) has simple component PSL2(7), a Mersenne prime case excluded from Walter's family. Working with classification pioneers Richard Lyons and Ronald Solomon, AxiomProver proved and formalized a brand new group theory result, Theorem 2.3 on preservation of simple tops, to complete the Unbalanced Group Theorem and close the full classification without unproved assumptions.
What to expect next
Axiom is publishing a comprehensive errata database alongside its Unbalanced Group Theorem repair paper in consultation with an advisory board including Richard Lyons, Ronald Solomon, and Dan Nakano so group theorists can inspect every corrected lemma. Beyond algebra, coordinating more than 150 agents across a 43 million line formally verified repository provides a blueprint for autonomous software verification where compiler kernels enforce global mathematical consistency across massive codebases.