Axiom says AI formalized the classification of finite simple groups in Lean: what is checked and what is not

A start-up says it has taught AI agents to check one of the longest proofs in mathematics. Axiom Math's project page announces a complete Lean formalization of the first-generation classification of finite simple groups, the result mathematicians call the enormous theorem. If the claim holds, it is a landmark for AI-assisted mathematics. Whether it holds is something outside experts have only begun to check. Axiom's page itself says every logical step is "checked by Lean's kernel," and no named mathematician outside the team has publicly endorsed the result in anything we could open.

What the theorem is, and why it is hard

The classification of finite simple groups lists the building blocks of all finite groups: infinite families, plus 26 sporadic exceptions, the largest of which, the Monster, has about 8 times 10 to the 53rd elements. According to OfficeChai's account of the announcement, the proof runs about 15,000 pages across more than 500 papers by roughly 100 mathematicians. A separate Lean project hosted by Renaissance Philanthropy puts it at "10,000 to 20,000 pages" spread over hundreds of books and papers, and calls formalization "a demanding standard" because every definition and omitted step must be made explicit.

The history adds a reason for caution. OfficeChai notes that the 1983 announcement of completion was premature, and that a gap involving quasithin groups was closed only in 2004. Smaller fixes kept appearing after. A computer-checked version is attractive precisely because human review of such a proof is so thin.

What Axiom reports

Axiom's project page reports 43.1 million lines of Lean, 2.05 million declarations and a corpus of 715 papers and books, of which 139 are source works. It says the work covers the first-generation proof, because the more systematic second-generation proof is incomplete. OfficeChai reports AI agent swarms worked for 24 days. The page's own milestone counts are inconsistent: one place says 100 milestones and another says 108, which is minor but worth noting in a result built on exactness.

The page names four core contributors, Dean Cureton, Vasily Ilin, Bhavik Mehta and Niels Voss, with Letong Hong as principal investigator and about 30 other contributors credited. The code is at github.com/AxiomMath/CFSG and an interactive proof map is at cfsg.axiommath.ai. Publishing both is the right instinct. Anyone can rebuild the project and watch the kernel accept or reject it.

The errors found

The most interesting claim is not the line count. While formalizing, the team says it found an issue in a published argument for the Unbalanced Group Theorem. Axiom's page cites a 35-page paper, "The Unbalanced Group Theorem" (Hexagon 2610.00575), which reports counterexamples to a closure assertion in that route and gives an alternative argument for the simple-group case, built on Solomon's 1976 theory of maximal 2-components. The team is also compiling errata with group theorists. OfficeChai reports 34 serious problems in all, with one needing real new mathematics.

If those errata stand up, they are the best evidence the exercise did more than re-typing. A formalization that finds real gaps has done work no skim read would. We have not independently checked the counterexamples, and the paper is Axiom's own.

What a Lean check does and does not prove

Lean's kernel verifies that each step follows from the previous ones, given the definitions and theorem statements in the code. It cannot verify that those definitions mean what a mathematician intends. If a definition of a simple group or a sporadic group is subtly wrong, the proof can be flawless and prove the wrong thing. That is why the page's own role for readers matters: experts need to compare the formal statements with the real classification. Our explainer on what verified means after Claude's library proofs makes the same distinction for software.

OfficeChai, our one outside account, relies on what "Axiom says" and quotes no independent mathematician. We found no outside audit.

A parallel, slower effort

Axiom is not the only group working on this theorem. The Renaissance Philanthropy page describes a Lean project in which, it says, humans set the targets and AI tools formalise the arguments, with the work split into self-contained sub-projects that outside contributors and AI tools can take on separately. Its planned outputs include open libraries of formalised group theory, the tooling used to build them and a structured benchmark for autoformalisation. The page lists Inna Capdeboscq and Damiano Testa on its team and describes Testa as a maintainer of Mathlib, the main mathematics library of the Lean theorem prover.

That contrast is useful. One effort is a start-up announcing a finished build. The other is an open, modular program aiming for understanding as well as certainty. If Axiom's work holds, the slower project may end up as the way the community checks it.

Why this matters for the race

For readers following capability, this is a different kind of result from a benchmark score. A benchmark asks whether a model gets a known answer. A formalization asks whether a swarm of agents can sustain a 43-million-line project to a state a machine can check. The checkable output is the point: even if Axiom's claim has flaws, they are findable.

What we would do

Treat the announcement as a strong lead, not a verdict. Read the repository README, wait for group theorists to comment on the statements, and watch whether the Hexagon paper and the errata survive review. If they do, the lesson is practical: AI works best in mathematics where a checker can say no.