AI Agents Formalize 15,000-Page Group Proof

Axiom, an AI mathematics startup, says swarms of AI agents have produced the first complete computer-checked proof of the Classification of Finite Simple Groups, a result whose human proof runs to roughly 15,000 pages. In a research post dated Oct. 26, the company said the agents wrote about 43.1 million lines of code in the Lean proof assistant over 24 days, and it published the code on GitHub.

Key takeaways

• Axiom says its Lean formalization covers the full first-generation proof, about 43.1 million lines and 2.05 million declarations.
• The repository says the proof is "sorry-free" and relies only on Lean's three standard axioms.
• The project surfaced 34 noteworthy deviations from the published literature, including a false claim in a 1986 memoir.

What is the Classification of Finite Simple Groups?

Finite simple groups are the building blocks of finite symmetry, often called its "periodic table." The theorem says every one of them is cyclic of prime order, alternating, one of 16 families of Lie type, or one of 26 sporadic groups, the largest being the Monster.

The proof is spread across more than 500 articles by about 100 mathematicians, according to Axiom. Daniel Gorenstein announced the classification complete in 1983, prematurely; the gap closed in 2004 when Michael Aschbacher and Stephen Smith published a 1,221-page treatment of the quasithin case. A shorter "second-generation" proof is still unfinished.

How Axiom's agents built the Lean proof

Axiom split the job into 108 milestones and about 380 smaller tasks. Its Slack channel opened Oct. 1, the first swarm went live Oct. 2, and the agents proved the Monster simple on Oct. 10. Progress then stalled: only one milestone had closed by Oct. 13, forcing a replanning effort.

The company says the agents used "a changing mix of models" but did not name them or disclose compute or cost. The work builds on Mathlib and includes about 1.2 million lines from the earlier Qiuzhen-CFSG project.

The GitHub repository is pinned to Lean v4.35.0-rc3, uses only Classical.choice, propext and Quot.sound, avoids native_decide and is licensed under Apache-2.0. Axiom says it aims to bring a full build under 24 hours.

Errors found in the published proof

The most serious problem involved the Unbalanced Group Theorem. Axiom says a lemma in Aschbacher and Smith's work fails for the group SL₂(5), and a closure claim in Walter's 1986 memoir breaks on PSL₂(49). Axiom says neither refutes the theorem; it repaired the argument by a different route and proved a new result to do so.

Group theorists Richard Lyons and Ron Solomon, veterans of the classification program, advised on the repair along with Dan Nakano.

Context: from Feit–Thompson to agent swarms

The benchmark until now was the Feit–Thompson theorem, a 255-page proof that Georges Gonthier's team verified in Coq in 2012 after six years. Axiom's claim is orders of magnitude larger and took weeks. It follows a run of AI-math announcements, including an OpenAI Navier-Stokes result that landed with an asterisk.

What's next

All claims so far come from Axiom; no independent group has yet reported rebuilding the proof. Axiom itself notes that the formal statement must be reviewed by humans to confirm it captures the intended theorem, and it says errata curation will continue under an advisory board.

FAQ

Did AI discover the classification?
No. Axiom says the theorem remains the achievement of the mathematicians who proved it. The agents translated the existing proof into machine-checkable code.

Is the proof independently verified?
Lean's kernel checks each step, according to Axiom, and the code is public. Outside confirmation that the formal statement is correct has not yet been reported.

References

• Formalizing the Enormous Theorem — Axiom (Oct. 26, 2026)
• The Classification of Finite Simple Groups, formalized in Lean — Axiom
• AxiomMath/CFSG — GitHub
• Axiom Math Releases 43.1M-Line Lean Proof of Group Classification — Unite.AI (Oct. 27, 2026)
• Classification of finite simple groups — Wikipedia