Chinese AI startup formalizes math's longest proof, open-sources 43.1M lines
Chinese-founded AI startup Axiom said in a GitHub-hosted announcement on Oct. 27 that its AI agents completed a full Lean formalization of the Classification of Finite Simple Groups, one of the longest proofs in mathematical history, in 24 days, producing about 43.1 million lines of code and open-sourcing the result. The project is a major test of machine verification for AI-generated mathematics at a time when models are producing proof drafts faster than mathematicians can independently review them. Also called the Enormous Theorem, the result classifies all finite simple groups. Its original proof spans about 15,000 pages in more than 500 papers by around 100 mathematicians, including work by John Thompson, Daniel Gorenstein, Michael Aschbacher, Stephen Smith, and later contributors. The theorem is widely used, but its fragmentation makes complete human verification impractical. Axiom, founded in March 2025 and led by CEO Carina Hong, used its AxiomProver system to coordinate multiple agents. The company's founding mathematician, Ken Ono, said formal verification is becoming essential as systems increasingly operate on code and proofs that no single person can read. The team built on roughly 1.2 million lines of prior group theory code, including material associated with Tsinghua University and mathematician Shing-Tung Yau, and divided the argument into 108 milestones and about 380 subtasks. Agents handled code writing and dependency retrieval while mathematicians resolved mathematical blocks and engineers improved the workflow. The effort targeted the first-generation proof because the second-generation book series remains unfinished. It produced machine-checked evidence for critical steps, including the existence and simplicity of the Monster group. During verification, agents identified numerous issues in published literature, such as typographical errors, incorrect table entries, omitted assumptions and 34 documented deviations. In one key dependency, they found a counterexample to an assertion in John Walter's 1986 argument for the unbalanced group theorem. Axiom then developed an alternative proof route with help from Richard Lyons and Ronald Solomon, and published a new group-theoretic result on Hexagon. Axiom said Lean's kernel has validated the complete inference chain, but human review is still needed to confirm that the formal statement matches the intended theorem and to assess the errata. The result arrives amid broader debate over AI in mathematics, including OpenAI's public proof drafts and calls by Terence Tao, Yu Deng and other scholars for mathematicians to participate from the start of AI proof projects rather than clean up their outputs afterward. The project does not resolve all concerns about machine-generated mathematics, but it shows how large, historically verified proofs can be converted into reproducible, inspectable code. By making the proof machine-readable, Axiom's work offers a new trust mechanism for an era in which mathematical confidence may depend less on expert memory and more on independently checkable formal systems.
