Classification of Finite Simple Groups formalized in Lean by directed AI agents
Axiom Math released a sorry-free Lean proof of the Classification of Finite Simple Groups that follows the first-generation proof, about 43.1 million lines written over 24 days by swarms of AI agents directed by its mathematicians and engineers, whose agents also found counterexamples to a step in one published route to the Unbalanced Group Theorem.
- Lab
- Axiom Math
- Model
- AxiomProver agent system using an unnamed, changing mix of models
- Field
- Mathematics
- Date
- 2026-10-26
- Human collaborators
- Dean Cureton, Vasily Ilin, Bhavik Mehta, Niels Voss, Letong Hong, Colin Defant, Ken Ono
What was found
The classification states that every finite simple group is cyclic of prime order, alternating, of Lie type, or one of 26 sporadic groups. Its first-generation proof is spread over hundreds of papers and books, and the second-generation revision is incomplete, so the project formalized the first-generation proof. The README states the theorem through the classification statement of the TauCeti project, written outside Axiom, and says the proof builds on Mathlib and TauCeti with only Lean's three standard axioms and no native_decide. The announcement says about 1.2 million lines come from the Qiuzhen-CFSG project and that the work was split into 108 milestones and about 380 tasks, with lead agents decomposing arguments and reviewing the statements being formalized while other agents searched for existing results or wrote proofs. Formalizing Walter's argument, the agents found explicit counterexamples to a closure assertion it uses, and a companion paper by Colin Defant and Ken Ono gives an alternative argument for the simple-group case of the Unbalanced Group Theorem built on Solomon's 1976 theory of maximal 2-components, whose key step the announcement credits to AxiomProver.
Novelty check
This is a formalization of a known theorem and is graded as such: the classification was announced complete in the early 1980s, and Aschbacher and Smith closed the quasithin case in 2004. arXiv, 2026-10-29: abs:"finite simple groups" AND abs:"Lean" returned 2 records, neither a complete formal proof of the classification. The announcement credits earlier Lean work, including about 1.2 million lines from the Qiuzhen-CFSG project, so partial formalizations existed and this builds on them. Within this registry Axiom Math has several earlier entries and none on group classification. The 2026-10-29 watch run surfaced it through an r/math comment and the Hacker News thread linked here.
Caveats and known objections
Graded claimed, following this registry's practice for large formalizations nobody outside the authors has rebuilt: every check recorded is Axiom's own. The README says the build fits in under 24 hours only with open changes to Lake and other optimizations not yet upstreamed, so a reader cannot yet rerun it with released tools, and no independent replay, second-kernel check or Palomar registration was found. Taking the statement from TauCeti means the theorem's wording was not written by the people who proved it, the strongest part of the record, but nobody independent is on record as confirming that the release proves that statement without extra hypotheses; the announcement notes that Lean can verify results proved under assumptions not yet established and says the project counted itself complete only when none remained, which is Axiom's account. The project lists 34 noteworthy deviations from the published record, most described as minor, the largest being the Unbalanced Group Theorem gap, and the announcement's milestone count of 108 differs from the 100 on the project page. The companion paper carries the venue's labels 'Primarily human-written text' and 'Human understanding: all parts' and its abstract does not mention AI, while the announcement credits its Theorem 2.3 to AxiomProver, so the two framings differ on who did the new mathematics. The models are not named. Autonomy is collaborative rather than ai-led: agents wrote the Lean and proved at least one new lemma, but human mathematicians investigated the obstructions, consulted the group theorists Richard Lyons and Ron Solomon, and wrote the paper resolving the most substantial one.
No independent check is recorded on this entry yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Claimed and Collaborative.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Community discussion
Graded claimed for verification and collaborative for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Classification of Finite Simple Groups formalized in Lean by directed AI agents. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-10-26-cfsg-lean-axiomBibTeX
@misc{whataifound-axiommath-2026-axiom,
title = {Classification of Finite Simple Groups formalized in Lean by directed AI agents},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Axiom Math. Verification: Claimed. Autonomy: Collaborative.},
url = {https://whataifound.org/finding/2026-10-26-cfsg-lean-axiom}
}