Axiom Math's AI agent swarms formalize the Classification of Finite Simple Groups in Lean in 24 days

For more than four decades, the Classification of Finite Simple Groups has stood as the largest cooperative achievement in the history of pure mathematics. The theorem identifies every possible basic building block of finite symmetry: every finite simple group is cyclic of prime order, alternating on at least five symbols, a member of one of sixteen infinite families of groups of Lie type over finite fields, or one of exactly 26 isolated sporadic groups. The original human proof extends across roughly 15,000 pages in more than 500 articles by about 100 mathematicians, a scale that earned it the nickname the enormous theorem.

That scale has always carried risk. A proof spread over hundreds of journal articles, written by dozens of authors across decades, is difficult for any single person to hold in view. Daniel Gorenstein announced completion of the classification in 1983, but a key case for quasithin groups was not filled until 2004, when Michael Aschbacher and Stephen Smith published a 1,221-page treatment. The historical record therefore already contains a cautionary tale about gaps surviving for years inside an argument the community believed was finished.

On October 26, 2026, Axiom Math, an AI startup based in Palo Alto, published what it describes as the first complete computer-checked proof of the Classification of Finite Simple Groups. Axiom said engineers and mathematicians at the company directed swarms of dozens of AI agents over 24 days, producing approximately 43.1 million lines of code in the Lean proof assistant. The company announced the release on X on October 27, 2026, with the blog post carrying the earlier date.

The project page lists 43.1 million lines of Lean, 2.05 million declarations and 715 papers and books in its corpus. Axiom's system, called AxiomProver, is described not as a single model grinding through pages but as a multi-agent architecture in which different agents handle decomposition, search, proof writing and review. The work follows the first-generation proof and incorporates roughly 1.2 million lines from the earlier Qiuzhen-CFSG project, building on the Mathlib library.

Key Facts

Crypto Briefing reported on October 27, 2026 that Axiom Math announced the completion on October 26, describing the output of approximately 43.1 million lines of Lean code as the largest Lean codebase ever created. The public GitHub repository is described as a sorry-free Lean4 proof pinned to version 4.35.0-rc3, using only the standard axioms Classical.choice, propext and Quot.sound, with no native_decide, under an Apache-2.0 license. Core contributors are named as Dean Cureton, Vasily Ilin, Bhavik Mehta and Niels Voss, with Letong Hong as principal investigator and Carina Hong as founding chief executive.

The coordination record is unusually detailed. On October 1, 2026, Axiom opened a dedicated Slack channel and divided the project into 108 milestones and about 380 smaller tasks. The first swarm went live on October 2, with agents claiming milestones through GitHub issues and reporting completed work in Slack. Lead agents decomposed difficult arguments, other agents searched for existing results or wrote Lean proofs, and an agent could delegate missing prerequisites to other agents. Human mathematicians investigated mathematical obstructions while engineers kept the system productive. The online proof map now shows 100 milestones.

Unite.AI reported on October 27, 2026 that translating the literature into Lean exposed problems in the published arguments. Most were minor: typographical errors, errors in tables, dropped hypotheses. But Axiom counted 34 noteworthy deviations from the published record that needed to be resolved, the most substantial relating to the Unbalanced Group Theorem. On October 10 the swarm proved the Monster simple and formalized its existence through the Griess algebra, an algebra of dimension 196,884 used by Robert Griess in 1980 to construct a group with approximately 8 x 10^53 elements.

The most serious finding concerned John Walter's 1986 Unbalanced Group Theorem. Agents found explicit counterexamples to a closure assertion, starting from PSL2(49), whose field involution has centralizer PGL2(7); the operation yields PSL2(7), which is excluded because 7 is a Mersenne prime. Axiom states that the theorem itself and the classification stand. The team built an alternative route from Ronald Solomon's 1976 theory of maximal 2-components. A 35-page paper titled The Unbalanced Group Theorem, by Colin Defant and Ken Ono, appeared on the Hexagon preprint server on October 27, 2026.

Axiom also reports a recurring failure mode. Early milestones concealed enormous prerequisites that agents had assumed rather than proved, and an agent could prove a proposition that was not the exact one needed, quietly adding an unproven premise. The team deleted tens of thousands of lines before restarting on a sounder plan. Axiom says the errata list will be published in consultation with expert group theorists. Richard Lyons and Ronald Solomon were consulted and sit on an advisory board for the errata, alongside external adviser Dan Nakano.

Analysis

The headline number invites skepticism, and some of it is warranted. Neural Brew reported on October 27, 2026 that it could not verify that the proof fully recompiles or that the final statement matches the intended theorem, and that no complete independent review had been published at the time of its article. The characterization of the longest proof in history is Axiom's own. The errata list has not been published in detail, so the total number of errors is not verifiable, and Crypto Briefing noted that its figure of more than 2,000 errors does not appear in Axiom's own blog post, which counts 34 noteworthy deviations and describes most issues as minor.

Those caveats are real but they do not cancel the substance of the claim. A Lean proof is not an essay that can persuade by prose; it is a formal object whose every deduction is checked by a machine. The repository is public, pinned to a specific toolchain version, and restricted to three standard axioms. That combination is designed to be audited, and the absence of an audit so far is a statement about elapsed time, not about the artifact's quality. The formalization also does not start from scratch, reusing about 1.2 million lines from Qiuzhen-CFSG, which means the marginal contribution is the remaining roughly 42 million lines plus the integration and repair work.

What this really means is that the bottleneck in formal mathematics has shifted from writing proofs to specifying statements. Lean checks deductions, not meaning: humans still need to verify that the final theorem says what the classification says. A verified artifact can be perfectly sound and still formalize the wrong proposition, which is precisely the failure mode Axiom says its own agents stumbled into repeatedly before the team deleted tens of thousands of lines. The 34 deviations matter because they are exactly the kind of defect that machine checking is good at surfacing and bad at interpreting. A dropped hypothesis or a table error is invisible in prose and fatal in Lean.

The Unbalanced Group Theorem episode is the strongest evidence in the release. Agents did not merely transcribe; they found explicit counterexamples to a closure assertion in a 1986 result, traced the obstruction to a Mersenne prime exclusion, and then followed an alternative route from Solomon's 1976 work. The bigger picture here is that the value of formalization is not certification of what mathematicians already believe but discovery of where the published record is thinner than its reputation. A 40-year-old gap found by a swarm in 24 days is a claim about the auditability of modern mathematics, not just about the capability of a startup.

Why It Matters

The classification is load-bearing infrastructure. Hundreds of results across group theory, representation theory and combinatorics are stated as consequences of it. Any project that depends on a case analysis of finite simple groups inherits whatever uncertainty sits inside the enormous theorem. A machine-checked version, even one awaiting independent rebuild, gives the community something it has never had: a single artifact in which every step is explicit and every dependency is a line of code rather than a citation to an article in a journal that may have dropped a hypothesis in 1986.

The method matters as much as the result. Axiom divided a multi-decade human effort into 108 milestones and roughly 380 tasks, then let dozens of agents claim work through GitHub issues while humans handled obstructions. That is a coordination pattern, not a mathematical insight, and it is reproducible. The company says the system used a continuously adjusted multi-model combination without disclosing which underlying models. Neural Brew contrasted Axiom's approach, mechanically verifying a known result and correcting parts of it, with OpenAI's claims the day before of new mathematical results. The two are different bets about where AI contributes: producing new theorems versus making old ones trustworthy.

There is also an institutional dimension. Axiom is putting the errata under the oversight of Lyons and Solomon, two of the central figures in the classification's later consolidation, along with Dan Nakano. That is a deliberate choice to route the disputed findings through the community that owns the literature rather than announce them unilaterally. Whether the community accepts the 34 deviations as genuine corrections or contests them will be the real test, and the unpublished errata list is the document to watch.

Next Up

The immediate tests are concrete. An independent group needs to rebuild the repository from scratch and confirm it compiles against the pinned toolchain, and reviewers need to check that the formal statements match the intended theorems rather than a weaker variant. The errata list, promised in consultation with expert group theorists and overseen by the advisory board, has not been published in detail. Until it is, the total error count remains unverifiable and the 34 notable deviations rest on Axiom's accounting.

Beyond that, the project sets a precedent for how large formalizations get done. Axiom has demonstrated that a coordinated swarm can traverse a corpus of 715 papers and books in 24 days, generating 2.05 million declarations. The open question is whether the same approach scales to results that have no published proof to follow, and whether the audit culture that machine checking enables becomes standard practice for theorems the field currently takes on trust.