Axiom Math Formalizes the 15,000-Page Classification of Finite Simple Groups in 24 Days

Axiom Math says it has produced the first computer-checkable proof of the classification of finite simple groups (CFSG), the result known as the “enormous theorem”, whose original proof runs to roughly 15,000 pages across more than 500 papers built by about 100 mathematicians over decades. In 24 days, dozens of AI agents wrote around 43.1 million lines of Lean code to formalize that body of work, with mathematicians involved in the original classification taking part.

The process did not just transcribe. Axiom reports 34 substantive discrepancies with published mathematics, counterexamples to some claims, alternative proofs where the originals broke, a new group-theory result needed for its chosen route, and cases where agents corrected faulty reasoning and supplied the missing argument. The code and materials are open for independent review.

Axiom Math: The Enormous Theorem, Formalized