Axiom Math Deploys AI Agents to Formalize Enormous Theorem in 24 Days

This time, AI not only completed a large-scale formal mathematical proof but also discovered new breakthroughs in previous research.

Edited by | Neo

Over 100 top mathematicians spent decades writing 15,000 pages of proofs.

Now, AI has transformed one of the most massive projects in the history of human mathematics into over 43 million lines of computer-verifiable code in just 24 days.

Even more astonishingly, while checking these proofs left behind by mathematicians, the AI identified an argument flaw that had persisted for nearly 40 years.

This is not an Olympiad math problem, nor a mathematical paper of a few dozen pages, but the Classification Theorem of Finite Simple Groups, known as the "Enormous Theorem."

Starting from the mid-20th century, hundreds of mathematicians participated in this research. In 1983, mathematician Daniel Gorenstein announced that the classification work was complete, but it was later discovered that there were still gaps to be filled. It wasn't until 2004 that mathematicians used another 1,221 pages of proof to fill a critical gap.

On October 26, AI mathematics company Axiom Math announced that dozens of AI Agents, organized by human mathematicians and engineers, completed the Lean formalization of this Enormous Theorem in 24 days. This generated approximately 43.1 million lines of code and 2.05 million formalized statements, providing the first computer-checked proof covering the entire classification theorem.

Mathematical reasoning originally scattered across more than 500 papers has now been organized into a formal system capable of step-by-step verification. Even more surprisingly, during this process, the Agents not only found errors in historical papers but also participated in constructing a new result in group theory.

Axiom's publicly released project on the formalization of the Classification Theorem of Finite Simple Groups includes approximately 43.1 million lines of Lean code, 2.05 million declarations, 100 milestones, and involves 715 references. Source: Axiom Math official website.

What exactly did the mathematical community spend decades proving?

To understand the difficulty of this work, we must start with "symmetry."

A square piece of paper, when rotated 90 degrees, perfectly coincides with its original shape; the same applies to rotations of 180 or 270 degrees. Mathematicians call the structure formed by these rotation operations and their combinations a "group." From geometric figures to particle physics, group theory provides a universal language for studying symmetry.

Complex finite groups can, in a certain sense, be decomposed into more fundamental parts. Just as integers can be factored into prime numbers, these indivisible "elementary particles" are called finite simple groups.

The Classification Theorem of Finite Simple Groups answers a seemingly naive question: What are all such elementary particles?

The final list includes cyclic groups of prime order, alternating groups, 16 infinite families of Lie-type simple groups, and 26 special "sporadic simple groups." Among them, the largest, the "Monster Group," has approximately $8 \times 10^{53}$ elements. Proving its existence alone was once a major achievement in mathematics.

Schematic diagram showing relationships among some "sporadic simple groups." Here, M at the top represents the largest sporadic simple group, the "Monster Group," while other nodes represent different sporadic simple groups.

Finding these groups is only half the job. The real challenge lies in proving that besides the types listed, there cannot be a 27th sporadic simple group, nor any undiscovered new type.

In 1963, Walter Feit and John Thompson proved in a 255-page paper that the order of all non-abelian finite simple groups is even, opening a breakthrough for subsequent classification. In 1972, Gorenstein proposed a 16-step research plan; in 1983, he announced the completion of the classification. The gap in the proof for quasi-thin groups remained until it was filled by Michael Aschbacher and Stephen Smith in 2004, with further corrections appearing in 2008.

The massive proof resembles a network of relationships spanning decades: one paper cites a theorem from another, which in turn relies on earlier lemmas. Many steps omitted conditions that authors considered obvious. Even if each paper looks reasonable individually, it is difficult for a single person to check every connection in the entire system.

What Axiom aimed to do this time was to transform all these connections into proofs verifiable by computers.

24 Days of Agent Engineering, Nearly Dragged Down by "Correct Proofs"

This was not about having a large model read 15,000 pages and then spit out tens of millions of lines of code in one go.

On October 1, Axiom opened a dedicated Slack channel, utilizing existing Lean base libraries and mathematical literature to organize a proof roadmap: 108 milestones and approximately 380 specific tasks. On October 2, the first batch of Agents began claiming tasks via GitHub Issues.

Some Agents were responsible for decomposing theorems, others for searching existing results, generating Lean proofs, reviewing propositions, and integrating code. When encountering incomplete prerequisite theorems, Agents could continue delegating tasks to other Agents. Human mathematicians handled key obstacles, while engineers coordinated these continuously working systems.

These Agents were coordinated by AxiomProver, a mathematical proof system independently developed by Axiom. The project adopted a constantly adjusted multi-model combination, but did not disclose the specific underlying model names. Compared to relying on a single model for reasoning, this system emphasized task decomposition, proof generation, and collaborative verification among different Agents.

Treemap of Axiom's formalization engineering for the Classification Theorem of Finite Simple Groups, displaying the scale of Lean declarations and code in different mathematical modules. Source: Axiom Math.

Shortly after work began, a tricky problem emerged: the Agent could prove a mathematical proposition, but not necessarily the one the project actually needed.

For example, while the original requirement was to prove that a bridge could safely support heavy trucks, the Agent first added an assumption: "Assume the bridge piers are sufficiently sturdy." With this premise in place, it smoothly proved that the truck could pass through, and even Lean accepted the entire derivation.

The problem, however, was that whether the bridge piers were actually sturdy enough had never been proven.

Similar issues recurred repeatedly in the early stages of the project. Some mathematical tasks that appeared complete had silently introduced unproven premises. Axiom was forced to delete tens of thousands of lines of code built upon these assumptions and reorganize the work.

As the codebase expanded, Lean's verification speed began to lag behind the Agents' output. Modifying a foundational theorem could force all dependent code to be re-verified. To address this, engineers introduced shared build caches and parallel verification mechanisms, allowing different Agents to reuse already confirmed results as much as possible.

On October 10, good news arrived in the team's Slack channel: "WE PROVED MONSTER IS SIMPLE." The Agent had completed the formalization of the simplicity of the Monster group and also formalized its existence via Griess algebras.

But three days later, project progress suddenly slowed down. On October 13, despite dozens of Agents continuously generating code, the team completed only one milestone proof task for the entire day.

The issue lay in task decomposition. The remaining mathematical challenges were too complex; beneath each major problem lurked many unresolved sub-problems. While the Agents could constantly write new proofs, they struggled to determine how many key steps had actually been solved and how far they remained from the final goal.

Axiom had to readjust its strategy, breaking down complex proofs into smaller, more explicit tasks, and requiring the Agents to explain how these small proofs would combine step-by-step to ultimately yield the required conclusion.

AI Digs Up 40-Year-Old Issues and Adds a New Proof

When the proofs delved into the deepest layers of historical literature, the Agent discovered something more troublesome than task scheduling: the original mathematical papers themselves might contain errors.

Human mathematicians often omit familiar reasoning, but Lean requires every premise to be explicitly stated. Axiom statistics show that there were 34 notable discrepancies in the literature that needed to be addressed during the formalization process, ranging from typos and missing conditions to substantive issues requiring re-derivation.

One example appeared in Aschbacher and Smith's work on "quasi-thin groups." A lemma in the original text asserted that two quantities were equal, but the Agent found a counterexample using the group SL₂(5): one quantity was 1, while the equation required it to be 2. Changing the equality to an inequality could fix the lemma, but subsequent reasoning had relied on that equality. The team had to expand the scope of the preceding argument and re-handle the affected cases.

A larger obstacle came from John Walter's 1986 research on the Unbalanced Group Theorem (UGT).

UGT is a crucial tool in the Classification of Finite Simple Groups (CFSG). It helps mathematicians infer the potential type of an entire group based on specific local structures within it. One of Walter's key inferences assumed that applying a certain operation to a specific family of groups would result in related simple groups that still belonged to the original family.

The Agent found a counterexample. Starting with PSL₂(49) and considering the involution induced by its field automorphism, the simple components of the relevant centralizer included PSL₂(7). However, the latter did not belong to the group family specified by Walter, meaning the original closure assertion failed.

This did not overturn the conclusion of UGT, but it meant that when following this proof path, one step required a different justification.

To resolve this, Axiom consulted group theory experts Richard Lyons and Ronald Solomon. Solomon's theory of maximal 2-components, proposed in 1976, provided key insights for the new approach.

Subsequently, the Agent constructed and formalized a new group theory result titled "Preservation of simple tops," proving that under the required conditions, comparing specific subgroups preserves the relevant simple group structure. This result was written into a 35-page paper titled The Unbalanced Group Theorem as Theorem 2.3, and combined with other existing results to complete the UGT proof required for the classification.

Interestingly, after the formalization was finished, Axiom's mathematicians discovered a shorter path in the first-generation proof method that could achieve the target conclusion without invoking this new theorem. Nevertheless, the new theorem and its complete proof were retained, becoming an additional mathematical contribution generated by this engineering effort.

Research on the Unbalanced Group Theorem participated in by the Axiom team. Theorem 2.3, "Preservation of simple tops," is a new mathematical result derived during this formalization process. Source: Paper The Unbalanced Group Theorem.

After 43.1 Million Lines of Lean, What Has Changed in Mathematical Proofs?

Ultimately, Axiom uploaded the entire project to GitHub, making approximately 43.1 million lines of Lean code public. The final classification proposition in the repository states: Every finite simple group is isomorphic to one of the groups listed in the catalog.

The project declared that the final proof contains no sorry—in Lean, this is a placeholder used to temporarily skip incomplete proofs. The final result relies only on standard axioms and can be checked step-by-step by the Lean kernel. Axiom also provided an interactive proof dependency graph, allowing researchers to trace which prerequisite theorems a conclusion depends on.

The final Lean code for the Classification of Finite Simple Groups released by Axiom. The final conclusion is obtained by calling underlying formalized proofs, backed by a proof engineering effort consisting of tens of millions of lines of Lean code. Source: Axiom Math / GitHub.

The foundation of this work also includes existing formalization projects such as Mathlib, TauCeti, and Qiuzhen-CFSG, with approximately 1.2 million lines contributed by Qiuzhen-CFSG. The accumulated research results of human mathematicians, early formalization infrastructure, and AI agents capable of parallel work have been integrated into a unified engineering pipeline.

For future mathematical research, a key change is that proofs can now be continuously maintained. Previously, citing the Classification of Finite Simple Groups (CFSG) theorem might involve hundreds of underlying references; now, researchers can trace the formalized dependency chain to verify exactly which definitions, conditions, and derivations are used.

Axiom’s public repository marks its review status as self-assessed by the team. External mathematicians can still check whether the formalized definitions accurately correspond to the original propositions and review the mathematical choices made within this massive undertaking. However, Lean already provides a capability previously difficult to achieve: subjecting tens of millions of lines of proof logic to uniform, mechanized verification.

Looking back at these 24 days, what deserves the most attention is not how much code the AI wrote, but that it began handling large-scale research work that was previously highly dependent on human experts: decomposing tasks, tracking proofs, discovering errors in older literature, and participating in constructing new proofs when old approaches failed.

Decades of accumulated mathematical knowledge are transforming from arguments scattered across papers into structures that can be programmatically checked, reused, and further extended. What Axiom demonstrated this time is a concrete attempt for AI to move from solving individual math problems to participating in the construction of entire mathematical theories.

References:

https://x.com/axiommathai/status/2115089794867040584

https://github.com/AxiomMath/CFSG/tree/main

https://hexagonmath.org/2610.00575

https://cfsg.axiommath.ai/

© THE END

Please contact this official account for authorization before reprinting.

Submissions or media inquiries: [email protected]

Open in WeChat