By Roman Aglaganov
The classification of finite simple groups is often called the longest proof ever written. It lists every “building block” of finite symmetry, and the original argument is spread across roughly 15,000 pages in more than 500 papers by about 100 mathematicians, completed over decades. On 27 October the start-up Axiom Math said it had turned the whole thing into a proof that a computer can check line by line.
What Axiom did
Axiom rewrote the proof in Lean, a programming language for mathematics in which every definition and step is precise enough for software to verify. According to the company, engineers and mathematicians directed “swarms of dozens of AI agents” for 24 days, from 2 October, and the result is about 43.1 million lines of Lean. The public repository describes it as a complete proof with no gaps left open (“sorry-free”, in Lean’s jargon).
The agents split the work into 108 milestones and about 380 smaller tasks. Lead agents broke hard arguments down and reviewed the statements being proved; others searched for existing results or wrote proofs. Human mathematicians handled the hardest problems, and engineers kept the system running. Axiom says one early lesson was that agents sometimes assumed difficult prerequisites instead of proving them, and the team deleted tens of thousands of lines built on those assumptions and restarted parts of the plan.
Errors in the original
Translating the proof into Lean exposed problems in the published papers. Most were small, such as typos, wrong table entries or missing conditions. But Axiom says it found 34 “noteworthy deviations from the published record”. In one, a lemma in a standard reference claimed two quantities were equal; the agents found a counterexample using a small group called SL₂(5).
The biggest problem was in a 1986 argument by John Walter for a step known as the Unbalanced Group Theorem. The agents found counterexamples to one of its claims. That did not make the theorem false, but it left a key step unjustified. Working with group theorists including Richard Lyons and Ronald Solomon, who helped build the original classification, Axiom’s system produced a different route, and with it what the company calls a new result in group theory. Axiom plans to publish the full list of errata with an advisory board of group theorists.
What is still unchecked
Lean checks the logic, but people still have to confirm that the formal statement says what mathematicians mean by the classification. Axiom’s statement comes from an outside project, TauCeti, and the company invites others to inspect it. Nobody outside Axiom has yet rebuilt the full proof, which takes close to a day of computing even with the company’s optimisations. Asked whether anyone had, chief executive Carina Hong told RuntimeWire: “Not yet.” Axiom is publishing the build files so others can try. The theorem itself was never in serious doubt; what is new is a version in which every step can be checked by machine.
