Axiom Math says AI agents formalized the classification of finite simple groups in Lean

Axiom Math, a US start-up building AI systems for mathematics, said on October 26, 2026 that it had produced a complete machine-checked proof of the classification of finite simple groups, one of the longest results in mathematics. The work was done in Lean, a proof assistant whose kernel checks every logical step.

What Axiom says it did

The classification states that every finite simple group is either cyclic of prime order, alternating, a group of Lie type, or one of 26 sporadic groups. Its original proof, completed by many authors over decades, is spread across thousands of journal pages. Axiom formalized this first-generation proof; a second-generation proof, being published in a series of volumes, is still unfinished.

According to the company's blog post, dozens of agents running on its AxiomProver system did the bulk of the writing over 24 days. Lead agents broke arguments into pieces and checked statements, while others searched for existing results or wrote Lean proofs, using a changing mix of models. Engineers and mathematicians steered the effort, investigated mathematical obstacles and handled the most consequential problems. Unite.AI reports that the first swarm started on October 2. The project page lists about 43.1 million lines of Lean and 2.05 million declarations, with the code published on GitHub.

Errors in the published record

Axiom reports 34 noteworthy deviations from the literature, most of them minor, such as typos, errors in tables or missing hypotheses. The most significant involved John Walter's proof of the Unbalanced Group Theorem, where agents found counterexamples to an assertion the argument relied on. Axiom says it repaired the gap with the help of a new result, and that group theorists Richard Lyons and Ronald Solomon were consulted. The company also flags a false equality in a lemma from Aschbacher and Smith's volumes on quasithin groups. It says none of this overturns the theorem itself, and it has published a full errata list.

Caveats

All figures come from Axiom's own materials, and the project's statistics page is not fully consistent; for example, it gives different counts of milestones and of source works in different places. Neither the blog post nor the outlets covering the announcement quote an independent assessment yet. As the company notes, Lean verifies the deductions, but humans still need to check that the formal statement and definitions faithfully match the mathematics. Axiom, co-founded by Carina Hong and Shubho Sengupta, raised $64 million in 2025.