AI math startup Axiom says it has fully formalized the Classification of Finite Simple Groups, often called the “Enormous Theorem”, in the Lean proof assistant. The original proof spans roughly 15,000 pages across more than 500 journal articles written by about 100 mathematicians over decades. Axiom says a swarm of AI agents produced a machine-checked version in 24 days and, along the way, found and repaired genuine gaps in the published literature. If it holds up, it is the largest formal verification ever completed.
Quick Take
- The scale: Axiom reports 43.1 million lines of Lean and 2.05 million declarations, drawing on 715 papers and books, built in 24 days.
- The fixes: The team documents 34 noteworthy deviations from the literature, including counterexamples to steps in published proofs that required new arguments.
- The standard: The proof is sorry-free, relies only on Lean’s standard axioms and avoids native_decide shortcuts, according to Axiom.
- The caveat: The work has not been independently rebuilt yet, and Axiom has not disclosed which models or how much compute it used.
What happened
Axiom detailed the project in a research post and released the code on GitHub alongside a project site. The company says its agent swarm went live on October 2, a day after the project began, and that by October 10 it had verified the simplicity of the Monster group, the largest sporadic simple group. After a slowdown around October 13, the team replanned the work and completed the formalization 24 days in. About 1.2 million lines came from the existing Qiuzhen-CFSG project, and the build uses Lean v4.35.0-rc3 with Mathlib. Axiom says a full build takes under 24 hours with a patched build tool.
The most interesting part is not the size but the corrections. Axiom’s write-up lists 34 noteworthy deviations from the published proof. Among them: a counterexample involving SL₂(5) in part of Aschbacher and Smith’s quasithin classification, and a counterexample built from PSL₂(49) to a closure step in a 1986 paper by Walter. To patch one gap, the agents produced a new result on the “preservation of simple tops”, drawing on Solomon’s 1976 work. Group theorists Richard Lyons, Daniel Nakano and Ronald Solomon advised the project. Axiom’s posts on X describe roughly 100 fixes and milestones, while the blog lists 34 noteworthy deviations and 108 milestones; the counts measure different things.
Why it matters now
Formalization at this scale was considered a decade-long human effort. Georges Gonthier’s team needed about six years to formalize the Feit–Thompson odd-order theorem in Coq in 2012, a single piece of the classification. Compressing a far larger job into weeks suggests AI can now turn trusted but unchecked mathematics into machine-verified knowledge at industrial speed.
It also changes what “proof” means in practice. Many results in group theory rest on chains of papers few living people have read end to end. A machine-checked version, with every dependency explicit, makes that foundation auditable and reusable for new work.
Who is most affected
Mathematicians working in finite group theory and formal methods gain most immediately, because the library makes decades of results checkable. AI labs pursuing reasoning see a new public benchmark for long-horizon agentic work.
| Stakeholder | Impact | Why |
|---|---|---|
| Group theorists | High | Decades of results become machine-checked, with documented gaps and repairs. |
| Formal methods community | High | A 43M-line library stress-tests Lean, Mathlib and build tooling at unprecedented scale. |
| AI reasoning labs | Medium | Sets a public, verifiable bar for long-horizon agentic work beyond benchmarks. |
The under-reported angle: does the formal statement mean what mathematicians meant?
A machine-checked proof is only as trustworthy as its formal statement. If the top-level theorem or a key definition in Lean subtly differs from the classical result, the proof can be correct and still not prove the theorem people care about. Axiom’s own repairs show that the published literature had real gaps, which also means translating it into Lean required judgment calls. Those choices need expert review. The project is also self-reported: Axiom’s CEO Carina Hong told RuntimeWire that no external party has reproduced it “yet”, and that the company is publishing build artifacts “to help and encourage external parties to independently reproduce it.”
What Grok and X are saying
Grok’s replies on X were enthusiastic. It explained the result as machine-checking the foundational “periodic table” of group symmetry and called it “a major boost for AI formal math”, noting that Axiom fixed gaps found along the way. One reply, however, said the agents produced the code “with no gaps”, which blurs an important distinction: the finished Lean proof has no unfilled steps, but Axiom had to repair real gaps in the literature to get there. Grok did not raise the lack of independent reproduction. Skeptics did. One user pointed out that “no outside group has independently rebuilt it”, and another argued the real question is “whether the formal statement still means what mathematicians meant.” Mathematicians and Lean users on X largely welcomed the open release of the code as the right way to settle those questions.
Our read: the openness is the strongest signal. Releasing a buildable artifact invites the scrutiny that marketing claims usually avoid. Until an outside group reproduces the build and experts sign off on the statement, treat this as a credible, extraordinary claim rather than settled fact.
About the analysis
Researched and written with AI assistance under the editorial responsibility of the i10X News team. The title image is an AI-generated illustration. Read our AI Use Policy. Spotted an error? Request a correction.
This independent, research-based i10x analysis synthesizes Axiom’s technical write-up and code release, press coverage and verified posts on X. Line counts, timelines and fixes are as reported by Axiom.
i10x Perspective
Axiom’s CFSG claim marks a turning point in how AI reasoning gets measured: not by benchmark scores but by verifiable artifacts that anyone can rebuild. If reproduction succeeds, the same agent-swarm approach could be pointed at other sprawling proofs, and eventually at critical software. The bar it sets for the rest of the industry is transparency; the open question is model and compute disclosure.
