Axiom's AI Agents Formalise Finite Simple Groups

Axiom Math says it has produced the first complete computer-checked proof of the Classification of Finite Simple Groups, a result in pure mathematics whose published proof runs to about 15,000 pages. According to Axiom’s research blog, engineers and mathematicians “directed swarms of dozens of AI agents” for 24 days, producing about 43.1 million lines of code in the Lean proof assistant.

On X, Axiom announced that “the largest math proof in human history is now computer-verified”. The Lean code is public in Axiom’s GitHub repository under the Apache 2.0 licence. No outside expert has yet published a review of the work.

Why this theorem matters

Finite simple groups are, in Axiom’s words, the “atoms” of finite symmetry: every finite group can be broken down into them. The classification says every one of them belongs to a few infinite families or is one of 26 exceptional “sporadic” groups, the largest of which is the Monster. Axiom says the original proof spans more than 500 articles by about 100 mathematicians, which earned it the nickname “the enormous theorem”. Results across algebra, number theory and combinatorics rely on it, often in a single line.

Lean is a programming language in which definitions and proofs can be written precisely enough for a computer to check every step. The repository describes a “sorry-free” proof, meaning no steps are left unproven, that follows the first-generation proof, relies only on Lean’s standard axioms, and states the theorem using the version from the TauCeti project. Axiom says building and checking it takes under 24 hours, using changes to Lean’s build tool that it plans to contribute back.

How the agents worked

Axiom says the project began with a Slack channel on 1 October and a proof map that split the work into 108 milestones and about 380 tasks. Lead agents broke down hard arguments, other agents searched for existing results or wrote Lean, and humans investigated problems. On 10 October the channel received the message “WE PROVED MONSTER IS SIMPLE”. The work built on Lean’s Mathlib library and includes about 1.2 million lines from an earlier project, Qiuzhen-CFSG.

The company is open about where things went slowly. On 13 October only one milestone closed, and engineers reorganised the plan into smaller, precisely stated theorems. Build times also became a bottleneck, because agents wrote proofs faster than Lean could recheck them.

What the formalisation found

Turning the published arguments into Lean exposed problems. Axiom says most were minor, such as typos, errors in tables and dropped hypotheses, but there were “34 noteworthy deviations from the published record”. In one example, agents found that a lemma in Aschbacher and Smith’s volumes on “quasithin” groups was false, using a counterexample involving the group SL₂(5), and the proof was rerouted around it.

The most serious case concerned the Unbalanced Group Theorem. Axiom says its agents found counterexamples to a step in John Walter’s 1986 proof, and that the repair needed a new result, proved by its AxiomProver system, set out in an accompanying paper. The company consulted Richard Lyons and Ronald Solomon, two group theorists who worked on the original classification, and says an advisory board including them will help curate an errata list it is making public.

A landmark claim that still needs expert checking

If it holds up, this is a striking result. When Georges Gonthier’s team formalised the Feit–Thompson theorem, one part of the classification, in 2012, it took six years. Axiom reports a far larger proof in 24 days, with human mathematicians guiding agents rather than writing the Lean themselves. The claim is also unusually checkable. Anyone with enough computing time can build the repository, and Lean will reject any invalid step. As Axiom puts it, “Humans inspect that statement and the definitions it uses to confirm that it expresses the intended classification; Lean checks the formal deductions establishing it.” That leaves two open questions: whether experts agree the formal statement says what the classification says, and how significant the 34 deviations prove to be. Axiom has not said what the project cost in computing. It fits a run of AI maths claims this month, from DeepMind’s AlphaProof Nexus to OpenAI’s 372 results and Microsoft’s KLS conjecture preprint. Funders such as the Simons Foundation, Anthropic and OpenAI are already funding efforts to help mathematicians evaluate AI tools of this kind.