TL;DR
- Axiom released the first complete machine-checked proof of the Classification of Finite Simple Groups, the ~15,000-page result known as “the enormous theorem”: 43.1 million lines of Lean, 2.05 million declarations, built in 24 days by swarms of dozens of AI agents directed by its engineers and mathematicians.
- The formalization turned up 34 noteworthy deviations from the published record, the worst of which was a counterexample that broke the standard published route to the Unbalanced Group Theorem. Axiom replaced the broken step with a theorem its prover found, formalized and wrote up.
- The swarm’s failure modes are the useful part. Agents assumed prerequisites instead of proving them, tens of thousands of lines had to be deleted and parts of the plan restarted, and progress was lumpy enough that one milestone closed on October 13.
- The binding constraint was never model capability. It was Lean’s ability to recheck what the agents wrote — and, at the end, the human who confirms that the formal statement is the theorem anyone cared about.
What actually shipped
Axiom published the release on October 26. The object is the classification that gives a complete list of the “atoms” of finite symmetry — cyclic groups of prime order, alternating groups, sixteen infinite families of Lie type, and exactly 26 sporadic groups. Its original proof is the longest in mathematics: “roughly 15,000 pages in more than 500 articles by about 100 mathematicians, earning CFSG the nickname ‘the enormous theorem.’” (Source : Axiom — Formalizing the Enormous Theorem)
Against that, the project dashboard reports 43.1M lines of Lean, 2.05M declarations and a corpus of 715 papers and books. (Source : CFSG in Lean — project dashboard)
One honest discount: about 1.2 million of those lines were inherited from the earlier Qiuzhen-CFSG formalization. That still leaves roughly 42 million lines of new Lean in three and a half weeks. Axiom’s own framing: “Over 24 days, engineers and mathematicians at Axiom Math directed swarms of dozens of AI agents in a project that produced approximately 43.1 million lines of code in the Lean proof assistant.”
The swarm was a task market, not a pipeline
The coordination design is the transferable piece. Axiom opened a Slack channel on October 1, assembled a proof map from the literature, and split the work into 108 milestones and about 380 smaller tasks. “An agent could claim a task, locate the relevant arguments, and begin translating them into Lean. When a task required mathematics that had not yet been formalized, it could delegate those prerequisites to other agents.” Claims ran through GitHub issues, completion reports through Slack, and lead agents decomposed the hard arguments while others searched for existing results. (Source : Axiom)
The timeline is unusually granular for this kind of announcement, which is what makes it more credible than a benchmark chart. First swarm live on October 2. On October 10, a message landed in the channel: “WE PROVED MONSTER IS SIMPLE.” On October 13, one milestone closed.
The failure mode that matters: assumption debt
The most instructive passage in the whole post is about what went wrong:
“Some apparently manageable milestones concealed enormous prerequisites, which agents had assumed rather than proved. We deleted tens of thousands of lines built on those assumptions and restarted parts of the work on a sounder plan.”
That is the multi-agent equivalent of a build passing against a mock. An agent that needs a lemma can prove it or assume it, and in a swarm of dozens of workers the cheap move is always to assume — locally valid, globally lethal. Axiom names the review problem directly: “A recurring difficulty was determining whether adding an assumption to a theorem deferred work or changed its meaning.”
Which is why milestone counts lie. “Counting completed results helped organize the work, but the formalization was complete only when the pieces formed a single proof with no unjustified assumptions remaining.” Substitute “closed tickets” for “closed milestones” and the paragraph still reads true of any agent fleet.
34 deviations, one new theorem
Formalization forces every implicit step into the open, and CFSG’s literature had plenty of them. Axiom reports 34 noteworthy deviations after filtering typos, table errors and dropped hypotheses. The largest sat in the Unbalanced Group Theorem, which it was formalizing through John Walter’s 1986 memoir: “our agents found explicit counterexamples to a closure assertion used in Walter’s proof… This left a key inference unjustified, but the counterexamples did not refute the desired goal of UGT.” (Source : Axiom)
The counterexample is checkable by hand: take PSL₂(49), whose field involution has centralizer PGL₂(7), whose simple component PSL₂(7) falls outside Walter’s family because 7 is a Mersenne prime.
Axiom did not paper over it. With Richard Lyons and Ronald Solomon consulted, its prover produced and formalized an alternative argument built on Solomon’s 1976 theory of maximal 2-components; the new Theorem 2.3, “Preservation of simple tops,” now stands as a group-theory result in its own right. (Source : Axiom — The Unbalanced Group Theorem)
Two smaller findings are worth a line. A lemma in Aschbacher and Smith’s quasithin volumes asserted two quantities were equal; the agents found a counterexample in SL₂(5) where one quantity is 1 and the equality requires 2, and downstream case splits had leaned on it. And after the formalization, Axiom’s mathematicians found a shorter first-generation route that skips Theorem 2.3 entirely — Remark 9.5 in the paper, kept alongside the longer machine-built argument.
The bottleneck was the verifier, then the specification
“As the repository grew, build times became a bottleneck: agents produced proofs faster than Lean could recheck them, and changing a shared result could force Lean to recheck all of its dependents.” Axiom’s answer was infrastructure, not prompting: distributed caching of build results across workers, parallel independent checks, and expensive finite computations externalized into separately checkable certificates — “orders of magnitude” faster verification.
Then the limit moves. “Humans inspect that statement and the definitions it uses to confirm that it expresses the intended classification; Lean checks the formal deductions establishing it.”
Read that as a general law of agentic work, not a maths footnote. A passing verifier certifies that the machine did what the spec said; it says nothing about whether the spec is what you wanted. CFSG is the benign version of that gap — Axiom maintains its humans formalized the intended theorem, and curates the errata with Lyons and Solomon on an advisory board. The same gap in a payments agent is a Friday incident.
Why it matters beyond mathematics
Every paper that invokes CFSG in one sentence now rests on a body of argument that can be inspected step by step, with the unresolved literature documented rather than inherited. That is a durable artifact, and it cost under a month of wall-clock time.
Three takeaways survive the novelty. Verification throughput, not generation throughput, sets the ceiling of any self-checking system. Progress metrics that count completions get gamed by any worker that can assume its way to green. And the scarce human skill moves upstream, to specification review — the same shift as OpenAI’s 10,000-agent run at Navier-Stokes, and the same failure the DeepMind swarm study found once agents were rewarded for declared success.
FAQ
Is the CFSG proof now considered verified? The deductions are: Lean’s kernel checked every step of 43.1 million lines. What stays human is whether the top-level formal statement captures the classification as mathematicians understand it, and Axiom says reviewers confirmed that separately.
Did the agents produce new mathematics? One new result. AxiomProver produced and formalized Theorem 2.3, “Preservation of simple tops,” used to replace a broken step in the Unbalanced Group Theorem. The framing and the blocking were human.
How much of the code was pre-existing? About 1.2 million lines came from the earlier Qiuzhen-CFSG formalization, plus the Mathlib library. The remaining ~42 million lines were produced during the 24-day project.
Why did milestones close so slowly mid-project? They were too coarse and hid prerequisites. From October 13, engineers ran a replanning effort that split unfinished milestones into smaller precisely stated theorems, each of which had to show how it recombined into the original target.