Axiom used AI agents to verify the longest proof in math history, the classification of finite simple groups, in Lean

The periodic table of symmetry

AI startup Axiom said in an Oct. 26 post, and in an announcement on X the next day, that it has computer-verified the Classification of Finite Simple Groups (CFSG) in the Lean proof language. The company describes it as the first complete computer-checked proof of the theorem.

The theorem gives the complete list of finite simple groups, the “atoms” of finite groups: cyclic groups of prime order, alternating groups on at least five symbols, sixteen families of groups of Lie type over finite fields and 26 sporadic groups. The largest sporadic group is the Monster, with about 8.08 × 10⁵³ elements.

Axiom@axiommathai

The largest math proof in human history is now computer-verified.

Today, Axiom announces a complete Lean auto-formalization of the Classification of Finite Simple Groups, the "periodic table of symmetry."

About 15,000 pages, built by over 100 mathematicians across generations.

A proof half a century in the making

According to Axiom, the original proof spans more than 500 papers by about 100 mathematicians and runs to about 15,000 pages. The roadmap began with Brauer’s 1954 address on the centralizers of involutions. The 255-page Feit-Thompson theorem came in 1963, Gorenstein laid out his sixteen-step program in 1972 and announced the classification complete in 1983. But a gap in the “quasithin” case was only closed in 2004, by Aschbacher and Smith’s 1,221-page work. A second-generation, more streamlined proof has been under way since the 1990s; its tenth volume appeared in 2023.

The Feit-Thompson theorem was verified in the Coq (now Rocq) proof assistant in 2012 by Georges Gonthier and colleagues at Inria. The full classification had never been computer-verified until now.

24 days with AI agents

The work began on Oct. 1, the first agent swarm went live on Oct. 2, and all 108 milestones were completed on Oct. 25. Swarms of dozens of AI agents ran on Axiom’s AxiomProver system. The work was split into 108 milestones and about 380 tasks. Lead agents broke arguments down and reviewed statements; others searched for existing results or wrote Lean proofs. Human mathematicians investigated obstructions, and engineers kept the system running.

The result is about 43.1 million lines of Lean code, including roughly 1.2 million lines from the earlier Qiuzhen-CFSG project. The Monster was proved simple on Oct. 10. The process wasn’t smooth: tens of thousands of lines were deleted after agents assumed some prerequisites without proof, and the plan was redone after only one milestone closed on Oct. 13.

34 deviations in published proofs

The agents found 34 noteworthy deviations from the published literature. Most were small issues such as typos, table errors or a dropped hypothesis. The most significant was in Walter’s proof of the Unbalanced Group Theorem (UGT): the agents found counterexamples to a closure assertion, such as the group PSL₂(49). The counterexamples didn’t refute the theorem, but they left a key inference unjustified. AxiomProver produced an alternative argument and a new group theory result, “Preservation of simple tops”; Axiom’s mathematicians later found a shorter route that avoids it.

An equality claimed in a lemma of Aschbacher and Smith’s quasithin work turned out to be false for the group SL₂(5) and was replaced with an inequality. The errors will be resolved with an advisory board of Richard Lyons and Ronald Solomon.

Caveats

The work follows the first-generation proof, because the second-generation proof is not complete. Lean checks every step, but whether the formal statement fully matches the theorem depends on human review, and Axiom itself warns against overstating progress. The code is open on GitHub under the Apache 2.0 license, and no independent verification has been done yet.