AI agents helped formalise a 15,000-page mathematics proof—but humans still have to inspect the statement
Axiom has released a 43.1-million-line Lean development for the classification of finite simple groups after a 24-day agent programme. The public artefact is machine-checkable; it is not yet an independently reviewed verdict on every modelling choice.
The short version
- What happened
- Axiom reports that dozens of agents and human mathematicians produced about 43.1 million lines of Lean in 24 days, connecting 100 milestones and material from 715 papers or books.
- Who it affects
- For mathematicians, the artefact can make dependencies and repaired gaps inspectable and reusable. For other research fields, it is evidence that agent systems can coordinate very large formal tasks, not proof that ordinary scientific claims can now be verified automatically.
- What remains unproven
- Company-led release
Keep in mind
Company-led release
No peer-reviewed full-project assessment yet
Human review of theorem statement and definitions remains essential
Trusted Lean kernel and imported foundations
43.1 million lines is scale, not a quality score
Historical proof routes may differ from the formal development
No cost or complete human-labour denominator published
Source analysis · 2 linked sources. Primary analysed source date: 26 October 2026.
Read the full report · 3 min The evidence, methods, implications and limitations
The release turns a dispersed literature into one checkable dependency chain
The classification of finite simple groups identifies the basic building blocks of finite symmetry. Its first-generation proof is spread across roughly 15,000 pages, more than 500 articles and decades of corrections. Axiom says its team directed swarms of dozens of agents from 2 October, with human mathematicians resolving obstructions and engineers keeping a shared dependency graph and distributed checking system working.
The released proof map reports 43.1 million lines of Lean, 2.05 million declarations, 100 milestones and 715 cited papers or books. The project also records 34 noteworthy deviations from the published record. Axiom says the most substantial concerned the Unbalanced Group Theorem; the development uses a replacement argument and the company has published an accompanying mathematical account for specialists to examine.[1][2]
Machine checking narrows the review problem; it does not eliminate it
Lean's kernel can verify that the final theorem follows from the definitions, hypotheses and previous lemmas encoded in the development. That is stronger than accepting an uncheckable generated explanation. It also guards against a common project failure Axiom describes: proving a nearby theorem under an extra assumption while leaving the intended milestone unresolved.
The remaining judgment is concentrated in the specification and trusted foundations. Mathematicians must inspect whether the formal theorem and definitions express the intended classification, whether imported results and certificates are represented correctly, and whether the new repairs deserve acceptance. The release is a major public artefact, but it is a company-led announcement rather than a peer-reviewed paper or completed independent audit.[1][2]
The distinction that matters
Where verification sits
The project separates mathematical specification from mechanical deduction.
Specify
Encode definitions, hypotheses and the final classification
Human mathematical judgment
Prove
Agents and experts connect the dependency graph
43.1 million lines of Lean
Check
Lean's kernel verifies every formal step
Machine-checked deductions, conditional on the specification