# Axiom Says AI System Formalized 15,000-Page Group Theory Proof By Simon Yoon Canonical URL: https://www.tokenpost.com/news/technology/42182 Published: 2026-10-28T00:59:35.000Z Updated: 2026-10-28T00:59:35.000Z Section: Technology > The 24-day project produced about 43.1 million lines of Lean code and found a significant gap in the Unbalanced Group Theorem proof. Axiom Math announced Oct. 26 that its AxiomProver system completed a formal version of the Classification of Finite Simple Groups that can be checked by computer. The company described the work as the first complete formalization of the result. The original proof spans about 15,000 pages and draws on more than 500 papers. More than 100 mathematicians contributed to the proof over several decades. Axiom’s effort took 24 days and produced about 43.1 million lines of Lean code. Lean is a language for expressing mathematical claims and proofs in a form a computer can check. The formalization encodes the argument as statements and deductions, allowing software to verify whether the deductions follow within the encoded proof. The classification says every finite simple group belongs to one of four categories: cyclic groups of prime order, alternating groups, groups from 16 families of Lie type, or 26 sporadic groups. These groups are building blocks from which finite groups can be broken down, making the classification a description of the possible types. AxiomProver uses multiple AI agents for tasks including decomposition, search, proof-writing and review. Expert mathematicians oversaw the review. A machine check can establish that the encoded deductions follow from the encoded assumptions, but it does not by itself establish that the formal statement captures the intended theorem. The same limitation applies to [other formalized AI math claims](). The formalization also exposed problems in published arguments. Axiom’s team found a significant gap in the proof of the Unbalanced Group Theorem, a component of the broader work, and developed a new segment of proof to close it. The team classified 34 departures from the published record as notable deviations. ## Links in this article - [other formalized AI math claims](https://www.tokenpost.com/news/technology/29219)