Startup Axiom Math says its AI agents formalized the roughly 15 000-page proof of the classification of finite simple groups, the “atoms” of symmetry, in 24 days using Lean, which checks every step, and found 34 significant discrepancies in published papers
Startup Axiom Math says its AI agents formalized the roughly 15 000-page proof of the classification of finite simple groups, the “atoms” of symmetry, in 24 days using Lean, which checks every step, and found 34 significant discrepancies in published papers
On October 27, Axiom released the project on GitHub. According to the company’s statement, dozens of agents from its AxiomProver AI system worked together under the supervision of mathematicians and engineers, producing about 43,1 million lines of Lean code.
A group is a collection of transformations, such as the 24 rotations that map a cube onto itself. Simple groups are indivisible “atoms”: every finite group can be broken down into them. The classification states that the list of these atoms is complete: it consists of infinite families and exactly 26 additional “sporadic” groups that fall outside those families.
About a hundred mathematicians wrote the classification proof across more than 500 papers. In 1983, Daniel Gorenstein announced its completion, but one case still depended on an unfinished manuscript. Michael Aschbacher and Stephen Smith closed that gap in 2004 with a 1221-page treatise. In a 2005 paper on highly complex proofs, Aschbacher asked: “It is impossible to write out a very long and complicated argument without making a mistake, so is such a ‘proof’ really a proof?”
Mathematicians have been writing a systematic version of the proof since the 1980s, but it remains unfinished, so Axiom tackled the original proof scattered across the literature. The team mapped the dependencies between theorems in the literature and divided the work into 108 milestones, each a theorem to prove. For some milestones, the agents assumed substantial results without proving them, and tens of thousands of lines built on those assumptions were deleted. Lean also accepts proofs that rely on additional unproven assumptions, so the team had to check that the statement actually proved matched the intended theorem.
A human reader uses experience to fill in steps omitted from a paper. Lean requires every condition to be explicit, which exposed errors, mostly minor ones such as typos and missing conditions. Axiom counted 34 significant discrepancies with the published text. The most substantial was in John Walter’s 1986 proof of the unbalanced group theorem, which identifies a whole group from its subgroups.
One step in Walter’s argument assumed that the simple part of a subgroup fixed by a symmetry of order two remains within the family of PSL₂(q) groups under consideration. However, PSL₂(49), which belongs to that family, has a symmetry of order two whose fixed subgroup is PGL₂(7). Its simple part, PSL₂(7), falls outside the family: 7 = 2³ − 1 is a Mersenne prime, and the family excludes such values of q. The error is confined to this step: neither the conclusion it was used to reach nor the theorem itself has been disproved.
The theorem can also be derived from results in the systematic version of the proof, but that route would have required formalizing many additional results in Lean. The team needed an approach compatible with the original proof. AxiomProver constructed a repair based on Ronald Solomon’s 1976 theory: it proves that, under the required conditions, comparing subgroups through the symmetries linking them preserves the simple part, replacing the assumption that the family is closed under this operation. Axiom describes this statement as a new result in group theory; its mathematicians later found a shorter derivation that does not require it.
Lean accepts or rejects each inference, while people check that the final statement expresses precisely the classification theorem. When RuntimeWire asked whether anyone outside Axiom had checked the proof, CEO Carina Hong answered “Not yet”: the build results have been published so that others can reproduce the verification.