Axiom Math says swarms of AI agents have produced the first complete computer-checked formalisation of the classification of finite simple groups, a proof that originally ran to about 15,000 pages across more than 500 articles. The agents wrote about 43.1 million lines of Lean code in 24 days, building on decades of human mathematics and finding real gaps in the published record along the way.
The enormous theorem
The classification of finite simple groups, known as the enormous theorem, says every finite simple group is cyclic of prime order, alternating, one of sixteen families of groups of Lie type, or one of 26 sporadic groups. Its original proof took about 100 mathematicians decades to assemble, and its scale is why a machine-checked version matters at all.
Axiom’s formalisation runs to about 43.1 million lines of Lean, with 2.05 million declarations and a corpus of 715 papers and books. It builds on Mathlib, the community library of formalised mathematics, and incorporates about 1.2 million lines from the earlier Qiuzhen-CFSG project, so the 24 days did not start from nothing.
The work was organised into 108 milestones and about 380 smaller tasks. Axiom opened a coordination channel on 1 October, the first agent swarm went live on 2 October, and lead agents decomposed difficult arguments while other agents searched for existing results or wrote proofs, delegating missing prerequisites to other agents through a shared repository.
Gaps found in the record
Translating the proof into Lean exposed problems in the published arguments. Most were minor, such as typographical errors, errors in tables or dropped hypotheses, but Axiom counts 34 noteworthy deviations from the published record, and the most substantial concerns the Unbalanced Group Theorem, a key step in the classification.
Approaching that theorem through John Walter’s 1986 memoir, Axiom’s agents found explicit counterexamples to a closure assertion the argument used. The argument assumed an operation kept the associated simple groups within a specified family, but starting from PSL2(49), the operation could produce PSL2(7), a group excluded from the family because 7 is a Mersenne prime.
The counterexamples did not refute the theorem itself, or even the conclusion of Walter’s Proposition II.5.9(ii), but they left a key inference unjustified. AxiomProver produced and formalised an alternative argument, stated as Theorem 2.3 on the preservation of simple tops, drawing on Ronald Solomon’s 1976 theory of maximal 2-components, with advice from Richard Lyons and Solomon.
After the formalisation, Axiom mathematicians found a substantial shortcut within first-generation methods, recorded as Remark 9.5, which reaches the required conclusion without Theorem 2.3. The accompanying paper retains both arguments, with their hypotheses and dependence on earlier mathematics made explicit, and Axiom says it will publish the errata found in the literature.
Why It Matters
The result matters for two different reasons. First, it shows agent swarms coordinating at a scale no single model could manage: dozens of agents, hundreds of tasks, and a shared repository, with engineers replanning when early milestones concealed enormous prerequisites that agents had assumed rather than proved.
Second, it shows machine checking doing something humans had not done: finding real holes in a celebrated proof. A formalisation does not by itself prove the formal statement captures the intended theorem, and human confirmation is still needed, but every logical step has now been checked by Lean’s kernel, which is a different kind of certainty.
The same formal-verification theme runs through other recent AI work, including OpenAI’s claims about machine-checked science proofs, as covered in our OpenAI science proofs report. The open question, echoed in research on how analysts defer to agents, as covered in our analysts and agents study, is how much human checking a machine-checked result still needs.
Background
Axiom says the classification remains the achievement of the mathematicians who discovered the groups and developed the arguments over decades. Its contribution is making the proof mechanically checkable, documenting the obstructions found, and supplying formalised arguments that resolve them, in the same spirit as safe agent execution work, as covered in our Akamai agent execution report.
Source: Axiom announcement Unite.AI report
0 Comments