Axiom says AI agents formalized the largest mathematical proof in Lean
The company released a 43.1-million-line formalization of the Classification of Finite Simple Groups and asked mathematicians to verify it independently.
Axiom has released what it describes as the first complete computer-checked proof of the Classification of Finite Simple Groups, a foundational result often called the largest proof in mathematics. The original classification spans roughly 15,000 pages in more than 500 papers by about 100 mathematicians.
According to Axiom, engineers and mathematicians directed dozens of AI agents for 24 days, producing about 43.1 million lines of Lean code. Lean checks whether every step follows from explicitly encoded definitions and assumptions, turning a literature-scale argument into one dependency graph.
The formalization surfaced typographical mistakes, missing hypotheses and 34 more substantial deviations from the published record. Axiom says one issue around the Unbalanced Group Theorem required major work and that the project yielded a new result in group theory.
A computer check is not the end of scientific review. The Lean statement itself must accurately express the accepted classification, and the formalization needs independent scrutiny. Axiom invited group theorists and the Lean community to rerun the checker and inspect the definitions. If validation succeeds, this would demonstrate AI agents handling a scientific project far beyond the scale one researcher could manually audit.
