On October 26–27, 2026, Axiom said it had produced a complete Lean 4 formalization of the Classification of Finite Simple Groups (CFSG). CFSG is the theorem whose first-generation proof is spread across thousands of journal pages written by roughly a hundred mathematicians. By Axiom's account, engineers and mathematicians directed swarms of AI agents for 24 days and generated about 43.1 million lines of Lean. Axiom also says the work turned up 34 "noteworthy deviations" from the published record, the largest affecting a published route to the Unbalanced Group Theorem (UGT), and produced a new group-theory result along the way.
Builders of AI systems should care because, if the claim holds, this is by far the largest machine-checked mathematical development ever produced, and it was produced mostly by agents. It would be strong evidence that agent swarms can carry out long-horizon, verifiable work at a scale no human team could. The question that matters is which parts are already guaranteed by the Lean kernel and which parts still rest on Axiom's own word.
What we checked
- Are the complete Lean artifacts publicly available? partly confirmed. There is a public Apache-2.0 repository, AxiomMath/CFSG. It is pinned to Lean v4.35.0-rc3 and says it is sorry-free, uses only Classical.choice, propext and Quot.sound, and avoids native_decide. The repository has a single commit, and the axiom and sorry checks are stated in the README; their output is not shown. [2][6]
- Is the formalization independently reproducible, and has anyone outside Axiom rebuilt it? unresolved. The README says
lake buildbuilds everything but depends on Lake changes that are 'not yet upstream', and aims for a build time under 24 hours. I found no report of a third party completing a build. The project site gives no build hardware and names no independent rebuilders. [2][6][7] - Have group theorists independently verified Axiom's claimed corrections and its new result? unresolved. The UGT paper (Hexagon 2610.00575) is a v1 preprint dated 2026-10-27 by Colin Defant and Ken Ono, who are both listed as Axiom contributors. It shows no sign of peer review. The errata page has no entries yet. The experts named, Richard Lyons and Ronald Solomon, are Axiom advisors, not independent reviewers. [4][5][1]
- (Added) Does the proved Lean statement cover the full classification theorem? partly confirmed. The target is the TauCeti ClassificationStatement: every finite simple group is isomorphic to a group on an explicitly constructed list. The lean-eval PR that adopted this statement says it does not require each listed group to be finite, simple or distinct, and that it inherits the correctness of TauCeti's group definitions. So the proof establishes the hard direction, which is completeness of the list. It does not establish that the list is exactly right. [3][2]
What we found
- Axiom's blog post describes 24 days of work starting October 2, 2026. It covers 108 milestones and about 380 smaller tasks, and folds in roughly 1.2 million lines from the earlier Qiuzhen-CFSG project. Lyons, Solomon and Nakano are listed as advisors. The post does not describe any formal external audit of the Lean development. [1]
- The AxiomMath/CFSG repository is public under Apache-2.0. It claims a sorry-free proof on Lean v4.35.0-rc3, built on Mathlib and TauCeti, using only the three standard axioms and no native_decide. At the time I checked it had a single commit. The README says the build depends on Lake changes not yet upstream and aims for under 24 hours. In other words, the code exists, but reproducing the result is a large and not yet documented job. [2]
- The theorem Axiom proves was not written by Axiom. It is TauCeti's ClassificationStatement, which Kim Morrison added as a benchmark problem in lean-eval on September 25, 2026. Because the statement is set independently, the 43M lines would not need to be trusted line by line. Only the statement, the axioms and the kernel check would need trusting. The PR notes that the statement asks only that every finite simple group be on the list, and inherits TauCeti's definitions of the Lie-type and sporadic groups. [3][2]
- The claims about the published literature have not been reviewed by anyone outside Axiom. The UGT paper is a v1 Hexagon preprint by Axiom contributors Colin Defant and Ken Ono. It reports counterexamples to a closure assertion in one published route to UGT and gives an alternative argument, and it says UGT itself still stands. The errata page Axiom promised currently says only that the list will be published later. [4][5]
- Axiom's own figures don't fully agree with each other. The project site lists 100 milestones in one place and 108 in another, and '715 papers and books' alongside a corpus panel showing 139 source works. The blog's count of 34 noteworthy deviations has not yet been backed by any public itemized list. [6][1]
- Independent news coverage so far repeats Axiom's claims. Unite.ai, for example, includes no quotes from outside experts and names no external team that rebuilt the proof. Searches turned up no public reaction yet from independent Lean or group-theory experts. [7]
What it means
For builders, the main lesson is how the result is set up. Axiom proved a statement someone else wrote, under the standard axioms, with no native_decide. That makes the claim far easier to check than a typical "AI did X" announcement. Trust then rests on three things: the TauCeti statement and definitions, Lean's kernel, and a successful rebuild. It does not rest on reading 43 million lines. Anyone building agentic systems for long, verifiable tasks should copy this pattern: fix the specification independently, forbid escape hatches, and let a small trusted checker do the judging. Until an outside party rebuilds the repository with the pinned toolchain and runs #print axioms on the final theorem, treat the result as very plausible but unconfirmed. Also note that the build currently relies on unreleased Lake changes.
The secondary claims need more caution. The literature corrections, the "34 deviations" and the new UGT argument are ordinary mathematical claims. They currently appear only in an unreviewed preprint by Axiom-affiliated authors and on an empty errata page, and they need group theorists outside Axiom to examine them. The theorem statement also covers only one direction: it shows every finite simple group is on the list, and depends on TauCeti's constructions being correct. Teams citing this result should say so precisely. Teams planning their own agent swarms should expect the bottlenecks Axiom reports, such as build throughput and replanning after flawed early assumptions, to dominate at this scale.
Still open
- Has any party outside Axiom rebuilt AxiomMath/CFSG with Lean v4.35.0-rc3 and confirmed with #print axioms that the final theorem uses only the three standard axioms?
- When will the Lake changes the build needs be upstreamed, and what hardware and wall-clock time does a full build take?
- Will independent group theorists confirm the UGT counterexamples (SL2(5), PSL2(49)) and Axiom's alternative argument, and will the itemized list of 34 deviations be published?
- Have TauCeti's definitions of the Lie-type and sporadic groups been independently reviewed, and will anyone formalize the converse direction, that every listed group is finite, simple and distinct?