Axiom Uses AI Agents to Verify Finite Simple Groups Proof in 24 Days

Baoyu (@dotey) · 2026-10-27 18

AI verifies the longest proof in mathematical history in 24 days: The theorem holds, but a flaw was found in one paper's approach. AI devised an alternative proof to fix it.

The proof spans 15,000 pages scattered across more than 500 papers. For decades, no single person has read it from start to finish. Is it actually correct? On October 26, AI mathematics company Axiom announced that they used dozens of AI agents over 24 days to rewrite the entire proof into code that computers can check step-by-step. Axiom states that all checks have passed.

This proof corresponds to the Classification of Finite Simple Groups, nicknamed the "Enormous Theorem." It took approximately 100 mathematicians decades to complete.

[What is this theorem about?]

First, let's define a "group." Consider a cube: you can find 24 rotations that leave it looking unchanged. Mathematicians call such a set of "operations that preserve appearance" a group. It is a tool for studying symmetry.

Just as integers can be factored into primes (which cannot be broken down further), groups can be decomposed into fundamental units called "simple groups." The Classification of Finite Simple Groups provides a complete list: every simple group either belongs to one of several infinite families with fixed patterns, or is one of 26 sporadic exceptions that belong to no family. The largest exception is the "Monster Group," which has $8 \times 10^{53}$ elements.

Finding these simple groups wasn't the hardest part; proving that the list contains all of them without omission was.

[Why use a computer to verify it?]

The proof is too long for humans to fully verify, and errors are unsurprising. In 1983, the lead mathematician declared the proof complete, only to discover later that a crucial section had never been written. This gap wasn't filled until 2004 with a 1,221-page book.

Axiom used the verification tool Lean. After translating the proof into Lean-readable code, the system checks each step rigorously: verifying if each step logically follows from the previous ones. When humans read papers, they often assume "this step is obvious," but Lean does not accept assumptions—it requires explicit derivation. In 2012, a team using similar tools spent about six years verifying just one 255-page paper within this theorem.

[What did the verification reveal?]

Conclusion first: The theorem itself is correct. The classification list remains valid.

The issue lay in the methodology of one intermediate paper. The overall proof relies on an intermediate result called the "Balance Theorem." Axiom translated the proof provided by mathematician John Walter in 1986. The AI discovered that a claim cited in Walter's proof was incorrect and provided a specific counterexample. It’s like solving a geometry problem where the final answer is right, but the solution uses an invalid condition midway through—the method needs changing.

Axiom consulted Richard Lyons and Ronald Solomon, who were involved in the original proof. Borrowing an approach from Solomon’s 1976 work, Axiom’s AI generated a new proof that bypassed the flawed step and successfully passed Lean’s verification. This new proof has been compiled into a 35-page paper.

Beyond this, most issues found were minor typos, table errors, or missing prerequisites. Axiom’s blog noted that 34 instances required specific handling, though the full list hasn’t been published yet. Axiom’s tweet stated more strongly that "hundreds of major errata" were corrected.

[How did the AI do it?]

Dozens of AI agents divided the labor: some broke large arguments into smaller lemmas, others searched for existing results, and others wrote Lean code. Human mathematicians handled complex mathematical hurdles where the AI got stuck, while engineers maintained the system. The final output consists of approximately 43.1 million lines of code (the tweet mentioned ~50 million, but the blog and website cite 43.1 million). About 1.2 million lines came from a previously open-sourced project by the Qiuzhen College team at Tsinghua University.

At times, the AI would treat unproven statements as known facts. Upon discovering this, Axiom deleted tens of thousands of lines of code and started over. Axiom did not disclose which specific AI models were used.

[Can we trust it completely?]

Lean guarantees that every logical step in the derivation is correct. However, it cannot determine if the initial statement defined in the code truly represents the Classification of Finite Simple Groups. If the translation of the theorem statement itself is flawed, then even a perfectly verified proof establishes something else entirely. This aspect still relies on human review. Axiom has invited group theorists and the Lean community to independently re-run the checks and verify the statement definition. Currently, this is Axiom’s own announcement; there has been no external independent verification yet.

Axiom Blog: https://t.co/pDcLp6CnWc Project Website: https://t.co/3ArK3yFvEt Axiom Tweet: https://t.co/BPNOxbaIqH

↳ Quoting @axiommathai (Axiom): 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.