Axiom Says AI Agents Machine-Checked the Classification of Finite Simple Groups in 24 Days

Axiom Math said on October 27 that it has completed a computer-checked proof of the Classification of Finite Simple Groups (CFSG) in the Lean proof assistant, the Russian-language channel AI ML Big Data reported. The original proof runs to roughly 15,000 pages across more than 500 articles by about 100 mathematicians, written over several decades. Axiom says engineers and mathematicians directed swarms of dozens of AI agents over 24 days. The agents wrote about 43.1 million lines of Lean 4, according to Unite.AI. The company has published the code on GitHub under an Apache 2.0 license.

The most substantive claim concerns errors. Axiom says the process found and corrected more than 2,000 errors in the existing literature, 34 of which it classifies as notable deviations. It also says it found a significant gap in the Unbalanced Group Theorem and wrote a new section of proof to close it. If independent group theorists confirm that gap, the project will have produced new mathematics, not merely a translation of existing proofs. The company also describes the output as the largest Lean codebase ever created. That description is Axiom's own, and no independent count has been published.

Three points need independent checking before the result can be treated as settled. First, the top-level Lean statement must match what mathematicians mean by the theorem. A formalized statement that is subtly weaker than intended can still pass Lean's check while proving the wrong thing. Second, the codebase must be free of placeholder gaps, known in Lean as sorry statements, and of non-standard axioms. Lean's own tooling can audit both automatically. Third, the 24-day figure excludes earlier infrastructure work and the human direction that Axiom itself acknowledges. Other groups are working toward the same goal. The FormaTheoria workflow, posted to arXiv in August, coordinates AI-assisted formalization with independent review, and a Renaissance Philanthropy-backed modular human-AI program also targets CFSG. Those projects give the field reviewers who can audit Axiom's claim.