The computer-checked "huge theorem": Axiom's AI agents formalize the classification of single finite groups within 24 days

Agents swarms translated into Lean a demonstration of 15,000 pages, or 43.1 million lines, and identified more than 2,000 errors, including a gap that had to be filled by new mathematics.

The Californian start-up Axiom announced that it had produced the first complete computer verification of the classification of finite simple groups, a central result of algebra whose original evidence spanned about 15,000 pages, distributed in more than 500 articles signed by about 100 mathematicians between the 1950s and the early 2000s. Its magnitude earned it the nickname of "huge theorem".

For 24 days, dozens of AI agents with separate roles (disaggregation of the problem, bibliographic research, writing of evidence, rereading) rewritten the whole in the Lean proof assistant, where each definition and each deduction must be explained and validated by the software kernel. The result, about 43.1 million lines, would be the largest Lean code base ever built.

Errors in a 40-year-old monument

The exercise revealed more than 2,000 errors, mostly minor; 34 were considered notable, and one of them, in the so-called unbalanced groups theorem, demanded to develop a new argumentation. The difficult cases were arbitrated by human mathematicians, including Richard Lyons and Ronald Solomon, who had participated in the original demonstration.