Axiom's agents formalize the classification of finite simple groups in Lean, and reroute a broken proof

Axiom Math says it has a complete, computer-checked proof of the classification of finite simple groups, the result that lists every "atom" of finite symmetry: cyclic groups of prime order, alternating groups, sixteen families of groups of Lie type and 26 sporadic groups. The original proof is usually put at around 15,000 pages across more than 500 articles by about a hundred mathematicians. Axiom's Lean version runs to 43.1 million lines and 2.05 million declarations, and the company says swarms of AI agents, directed by its engineers and mathematicians, produced it in 24 days.

The size is the headline, but two other things matter more. The theorem being proved was written down by someone else before the project started, and the formalization turned up a real gap in one of the published arguments it was following.

What exactly was checked

Formal proofs are only as good as their statements, so the statement is the first thing to read. Axiom did not write its own. The repository proves TauCeti.ClassificationStatement, taken from Tau Ceti, an AI-written Lean library incubated by the Lean FRO and the Mathlib Initiative. That statement is four lines: every finite simple group, in any universe, is isomorphic to one of the explicitly constructed groups indexed by CFSGIndex. The index fixes the parameter ranges for each Lie-type family and removes the usual small coincidences, such as naming B₂(q) and C₂(q) only once. The statement landed in Tau Ceti on September 25, a week before Axiom says it opened the project's Slack channel on October 1.

The proof is packaged as a challenge for Comparator, the same checking setup OpenAI used for its Exponential Time Hypothesis claim a day earlier. The challenge file states the theorem with sorry, the solution file proves it, and comparator.json permits only Lean's three standard axioms: propext, Quot.sound and Classical.choice. The README adds that the proof uses no native_decide, the tactic that hands computations to compiled code and so widens what has to be trusted. Heavy finite calculations are split out into certificate modules, which live in the repository as ordinary Lean files.

Two caveats are worth keeping in mind. The checked theorem is the "nothing is missing" direction: every finite simple group appears on the list. Axiom's write-up says the development also proves that the listed groups exist and are simple (the Monster's simplicity was a milestone on October 10), but that is not what the Comparator target asserts. And checking it yourself is not cheap. The README says a full lake build takes under 24 hours, and only with "a few open changes to Lake and some optimizations we plan to upstream soon", on a release-candidate toolchain (Lean v4.35.0-rc3). The public repository is also a single squashed commit, so the 24-day history described in the blog post cannot be read from it. As of this writing we have not seen an independent report of a full rebuild.

How the swarm worked

Axiom's account is unusually frank about what went wrong. The project started from existing Lean work, including about 1.2 million lines from the Qiuzhen-CFSG project, and a proof map built from the literature that split the work into 108 milestones and about 380 tasks. Agents claimed milestones through GitHub issues, delegated missing prerequisites to other agents and reported in Slack. Lead agents decomposed arguments and reviewed statements; others searched for existing results or wrote proofs, using "a changing mix of models".

The recurring failure was quiet weakening. An agent would prove a milestone under an extra hypothesis that nobody had proved, and Lean would accept it, because a conditional theorem is still a theorem. Early on, Axiom deleted tens of thousands of lines built on such assumptions. On October 13 only one milestone closed, and the team responded with a replanning pass in which agents had to break unfinished milestones into smaller statements and show how they would combine into the original with a short Lean proof. The other bottleneck was mundane: agents wrote proofs faster than Lean could recheck them, so Axiom built a distributed build cache so workers could reuse each other's results.

This is the most practical lesson in the post for anyone running agents on formal work. The kernel guarantees that each step is valid, not that the agent proved the theorem you asked for. Axiom's answer was review that compares the proved statement with the intended one and a single fixed top-level target, which is exactly what a harness has to enforce when nobody is reading every file.

The gap in the literature

Translating the proof exposed problems in the published record. Most were typos, wrong table entries or dropped hypotheses; Axiom counts 34 "noteworthy deviations". One example from Aschbacher and Smith's quasithin volumes: a lemma asserted two quantities were equal, and the agents found a counterexample in SL₂(5), where one was 1 and the other needed to be 2. Weakening the equality to an inequality broke some later case eliminations, which then had to be argued differently.

The serious one concerns the Unbalanced Group Theorem, a key step that identifies a minimal counterexample from the structure of an involution's centralizer. Axiom followed John Walter's 1986 memoir, and its agents found counterexamples to a closure assertion that the argument relies on. The simplest starts from PSL₂(49): the involution induced by the field automorphism has centralizer PGL₂(7), whose simple component PSL₂(7) is excluded from Walter's family because 7 is a Mersenne prime. The flaw does not make the theorem false, or even the conclusion of the proposition in question; it leaves one inference in that particular route unjustified, and UGT has other proofs.

Switching to one of those proofs would have dragged in second-generation results that also needed formalizing. Instead, after consulting Richard Lyons and Ronald Solomon, two of the group theorists behind the original classification, AxiomProver produced and formalized an alternative argument based on Solomon's 1976 theory of maximal 2-components. Its key step, a "preservation of simple tops" theorem, is written up in a 35-page paper contributed by Colin Defant and Ken Ono and labelled as primarily human-written. One detail undercuts the triumphal version slightly: after the formalization was done, Axiom's mathematicians found what they call a substantial shortcut within first-generation methods that does not need the new theorem at all (Remark 9.5 of the paper).

What is still missing

The full errata list is not out yet. The project site says it is being compiled with group theorists and "will be published here". Until it is, the 34 deviations are Axiom's count, without the details that would let specialists judge how serious each one is.

Even so, the shape of the claim is a good one. The target was fixed by an outside library before the work began, the axioms are the standard ones, the code is under Apache 2.0, and the mathematical repair is explained in a paper that group theorists can argue with. Whether 43 million machine-written lines are of any use to a human reading group theory is a separate question. As a check that the classification holds together as stated, it is a more inspectable kind of evidence than the theorem has ever had. It will be stronger still once someone other than Axiom finishes the 24-hour build.