Axiom announces it has verified in Lean the classification of finite simple groups, the longest proof in mathematics

Startup Axiom claims to have made computer-verifiable the classification of finite simple groups (often abbreviated CFSG), nicknamed “the enormous theorem”: a proof of roughly 15,000 pages, spread across more than 500 articles written by about a hundred mathematicians over several decades. The announcement dropped on X this Tuesday, October 27 at 3:34 p.m., Paris time, accompanied by a lengthy blog post dated the day before, an interactive proof map, and a code repository.

What this is about

A group describes symmetries, like the 24 rotations that leave a cube unchanged. Finite groups break down into indivisible “building blocks,” simple groups, much like integers into prime numbers. The classification says this list of building blocks is complete: cyclic groups of prime order, alternating groups (on at least five elements), sixteen infinite families of “Lie type” groups, and exactly 26 sporadic groups, including the largest, the Monster group. This result is used in many fields (algebra, number theory, combinatorics), but very few people can check the whole thing.

Axiom rewrote this proof in Lean, a proof assistant: a language where every definition and every logical step is written precisely enough for a program to check them. The project site shows 43.1 million lines of Lean and 2.05 million declarations.

How AI agents were put to work

Axiom’s story is above all one of organization. The project kicked off on October 1, 2026 with a proof map drawn from the literature and existing Lean code, broken down into 108 milestones and roughly 380 tasks. As early as October 2, swarms of several dozen AxiomProver agents, using a shifting mix of models, claimed tasks via GitHub tickets and reported back in Slack. “Lead” agents broke down difficult arguments and checked statements; others searched for existing results or wrote proofs.

Axiom doesn’t hide the failures. Seemingly simple milestones hid enormous prerequisites that the agents had assumed rather than proved: tens of thousands of lines were deleted. Recompilation time also became a bottleneck, solved by a shared caching system across machines. Humans remained at the center: mathematicians for substantive obstacles, engineers to keep the system running.

What the machine found

Formalizing forces you to make explicit what a human reader fills in themselves. According to Axiom, most of the issues found were minor (typos, wrong tables, forgotten hypotheses), but 34 notable discrepancies with the literature had to be resolved. The most serious concerns the Unbalanced Group Theorem, in John Walter’s 1986 version: the agents found counterexamples to a step in the reasoning, without refuting the theorem itself. With the help of Richard Lyons and Ronald Solomon, two historical specialists in the classification, another route was built from Solomon’s 1976 work. Axiom presents this as a new group theory result, described in a paper accompanying the publication.

Axiom promises to publish the complete errata list with a committee of specialists. Until it goes online, the total number of errors identified remains unverifiable.

Limits to keep in mind

Lean checks deductions, not the meaning of the statement: humans still need to verify that the final theorem and its definitions say what the classification says. Axiom acknowledges this in its text. As of this writing, no complete independent verification has been published, and we have not recompiled the repository ourselves. The formalization also doesn’t start from scratch: it incorporates roughly 1.2 million lines from the Qiuzhen-CFSG project and builds on the Mathlib library.

This announcement comes the day after the mathematical results claimed by OpenAI, which we covered here. The approach is different: OpenAI says it found new results, Axiom says it mechanically verified a known result and corrected parts of it.