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

Axiom says engineers and mathematicians directed swarms of dozens of AI agents to formalize the classification of finite simple groups (CFSG) in the Lean proof assistant, producing approximately 43.1 million lines of code over 24 days. Asked whether anyone outside the company has built and checked it, founder and CEO Carina Hong said: "Not yet. We are publishing the build artifacts to help and encourage external parties to independently reproduce it."

Axiom's blog post is dated October 26, 2026. According to Neural Brew, the announcement hit X on Tuesday, October 27, at 3:34 p.m. Paris time, with an interactive proof map and a code repository attached. The announcement is out; independent reproduction, Hong says, is still to come.

The enormous theorem, by the numbers

CFSG says every finite simple group is a cyclic group of prime order, an alternating group on at least five symbols, a member of one of sixteen infinite families of groups of Lie type, or one of exactly 26 sporadic groups. The largest of those is the Monster, with approximately 8 x 10^53 elements.

Axiom describes the original human proof as roughly 15,000 pages in more than 500 articles by about 100 mathematicians. Hence the nickname "the enormous theorem."

For scale, Axiom's own history lesson notes that the Feit-Thompson theorem, a 255-page paper from 1963, took Georges Gonthier's team six years to formalize in Coq, finishing in 2012. CFSG is roughly 60 times longer on paper. The agents needed 24 days.

The project site shows 43.1 million lines of Lean and 2.05 million declarations, according to Neural Brew. It also reports that the formalization incorporates about 1.2 million lines from the Qiuzhen-CFSG project and builds on Mathlib. The site records 715 papers and books catalogued.

One number does not agree with itself. Axiom's blog post says the plan began with 108 milestones and about 380 smaller tasks. The project site shows 100 milestones. The post gives no reconciliation, though a plan that was revised mid-project would explain it.

How the swarm worked

Axiom opened a Slack channel on October 1 and launched the first swarm of agents on October 2. Agents claimed milestones through GitHub issues and reported finished work in Slack. They used what the company calls a changing mix of models. Which ones is not stated.

It was not a straight line. On October 10, a message appeared in the channel: "WE PROVED MONSTER IS SIMPLE." On October 13, only one milestone closed, and Axiom says the targets were too coarse to show what mathematics remained, which prompted a replanning effort.

The most instructive admission is also the least glamorous. Some apparently manageable milestones hid enormous prerequisites that agents had assumed rather than proved. Axiom says it deleted tens of thousands of lines built on those assumptions and restarted parts of the work. Closing a milestone is not the same as proving its prerequisites. Tens of thousands of deleted lines make that point rather efficiently.

To get through build bottlenecks, engineers built a system that distributes cached build results across workers and runs independent checks in parallel. Expensive finite calculations were moved out into certificates that can be checked separately.

What the agents found in the literature

Translating the published record into Lean surfaced 34 noteworthy deviations that had to be resolved, according to Axiom. The most substantial involved the Unbalanced Group Theorem (UGT).

Two examples stand out. In Aschbacher and Smith's quasithin volumes, agents found a lemma asserting two quantities were equal and produced a counterexample in SL2(5), where one quantity was 1 instead of 2. In John Walter's 1986 memoir on UGT, they found explicit counterexamples to a closure assertion, starting with PSL2(49), whose field involution has centralizer PGL2(7) with simple component PSL2(7).

The claim goes further. AxiomProver produced and formalized an alternative proof of UGT built on Ronald Solomon's 1976 theory of maximal 2-components. Axiom calls the resulting statement, Theorem 2.3 ("Preservation of simple tops"), a new result in group theory. Its own mathematicians later found a shortcut within first-generation methods that reaches the UGT conclusion without it, recorded in Remark 9.5. A new theorem that its authors then route around is a very honest sort of milestone.

Humans stayed in the loop. Axiom says mathematicians investigated the most consequential reports, and that original CFSG contributors Richard Lyons and Ronald Solomon were consulted.

One scoping choice matters: Axiom formalized the first generation proof, because the second generation proof is not finished. Ten volumes had appeared by 2023, and at least twelve are expected.

What to watch

The first test is the boring one: does an outside group rebuild all 43.1 million lines and get a green check? How long a full build takes is not stated in the material Axiom has put out so far.

The second test is subtler: will group theorists agree that the definitions and final formal statement faithfully capture CFSG, without unintended loopholes? Also worth watching: when the complete errata list and counterexample database become available to the mathematical community.

And there is the matter of which models did the work. "A changing mix" is not a methods section. Show me the eval, not the vibe.