Axiom Math uses dozens of Agents to formalize the classification theorem of finite simple groups in 24 days, generating 43.1 million lines of Lean code

Dozens of agents took on a massive mathematical project in 24 days and even uncovered a flaw that had gone unnoticed for 40 years. Machine Heart Download the client for exclusive early access. October 28, 2026, 12:03:22, from Beijing. Updated October 28, 2026, 14:29:57.

Editor｜Neo

More than 100 leading mathematicians spent decades writing a 15,000-page proof.

Now, AI has taken only 24 days to turn one of the largest projects in the history of human mathematics into more than 43 million lines of code that can be verified step by step by computer.

Even more striking, while checking the proofs left by these mathematicians, the AI also uncovered a gap in an argument that had existed for nearly 40 years.

This is not an olympiad problem, nor a mathematical paper of a few dozen pages, but the classification of finite simple groups, known as the "Enormous Theorem."

Beginning in the mid-20th century, more than a hundred mathematicians took part in this research. In 1983, mathematician Daniel Gorenstein announced that the classification work had been completed, but it was later discovered that parts still remained unfinished. It was not until 2004 that mathematicians filled a key gap with a 1,221-page proof.

On October 26, the AI mathematics company Axiom Math announced that dozens of AI agents organized by human mathematicians and engineers had completed the Lean formalization of this enormous theorem in 24 days, generating about 43.1 million lines of code and 2.05 million formal declarations, and producing 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 that can be checked step by step. Even more unexpectedly, during this process, the agents not only found errors in historical papers but also took part in constructing a new result in group theory.

The formalization project of the classification of finite simple groups released by Axiom contains about 43.1 million lines of Lean code, 2.05 million declarations, 100 milestones, and involves 715 references. Image source: Axiom Math official website.

A square piece of paper, after being rotated 90 degrees, has exactly the same shape as before; the same is true for rotations of 180 degrees and 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 general language for studying symmetry.

Complex finite groups can, in a certain sense, be decomposed into more basic parts. Just as integers can be decomposed into prime factors, these "elementary particles" that cannot be further decomposed are called finite simple groups.

The classification theorem of finite simple groups answers a seemingly simple question: what exactly are all such elementary particles?

The final list includes cyclic groups of prime order, alternating groups, 16 infinite series of simple groups of Lie type, and 26 special "sporadic simple groups." The largest of them, the "Monster Group," has about 8×10^53 elements. Merely proving that it exists was once a major achievement in mathematics.

A schematic diagram of the relationships among some "sporadic simple groups." Among them, the M at the top represents the largest sporadic simple group, the "Monster Group," and the other nodes represent different sporadic simple groups.

Finding these groups is only half the work. The truly difficult part is proving that, apart from the types on the list, no 27th sporadic simple group is possible, and that no undiscovered new type exists.

In 1963, Walter Feit and John Thompson used a 255-page paper to prove that the order of every non-abelian finite simple group is even, opening a breakthrough for the subsequent classification. In 1972, Gorenstein proposed a 16-step research plan; in 1983, he announced that the classification was complete. The later gap in the proof for quasithin groups was not filled until 2004 by Michael Aschbacher and Stephen Smith, and further corrections appeared in 2008.

The enormous proof is like a network of relationships spanning decades: one paper cites a theorem from another, which in turn depends on earlier lemmas. Many steps also omitted conditions that the authors considered obvious. Even if each paper seems reasonable on its own, it is very difficult for one person to check every connection in the entire system.

What Axiom set out to do this time was to turn all these connections into proofs that a computer can verify.

The 24-day agent project, almost brought down by a "correct proof"

This was not a matter of having a large model read 15,000 pages and then spit out tens of millions of lines of code all at once.

On October 1, Axiom set up a dedicated Slack channel and, using the existing Lean foundation libraries and mathematical literature, put together a proof roadmap: 108 milestones and about 380 specific tasks. On October 2, the first batch of agents began claiming tasks through GitHub Issues.

Some Agents are responsible for breaking down theorems, some search existing results, some generate Lean proofs, and others review propositions and integrate code. When encountering prerequisite theorems that have not yet been completed, an Agent can continue to hand the task off to other Agents. Human mathematicians handle key obstacles, while engineers are responsible for coordinating these continuously working systems.

These Agents are coordinated by AxiomProver, a mathematical proof system independently developed by Axiom. The project adopted a continuously adjusted multi-model combination, but did not disclose the specific list of underlying models. Compared with relying on a single model to complete reasoning, this system places greater emphasis on task decomposition, proof generation, and collaborative verification among different Agents.

A treemap of Axiom's formalization project for the classification of finite simple groups, showing the scale of Lean declarations and code across different mathematical modules. Image source: Axiom Math.

Not long after work began, a thorny problem emerged: an Agent could prove a mathematical proposition, but not necessarily the one the project actually needed.

For example, the original requirement was to prove that a bridge can safely carry heavy trucks, but the Agent first added a condition: "Assume the bridge piers are strong enough." With this premise, it smoothly proved that the trucks could pass, and even Lean accepted the entire derivation.

But the problem was that whether the bridge piers were actually strong enough had not been proved at all.

Similar problems occurred repeatedly in the early stages of the project. Some mathematical tasks that appeared to be completed had actually quietly introduced unproved premises. Axiom had to delete tens of thousands of lines of code built on these assumptions and rearrange the work.

As the codebase expanded, Lean's checking speed also began to fall behind the Agents' output. Modifying a foundational theorem could force all code depending on it to be rechecked. Engineers therefore introduced a shared build cache and parallel verification mechanisms, so that different Agents could reuse already confirmed results as much as possible.

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

But three days later, the project's progress suddenly slowed down. On October 13, although dozens of Agents were still continuously generating code, the team completed only one staged proof task for the entire day.

The problem lay in task decomposition. The remaining mathematical difficulties were too complex, and beneath one major problem hid many unresolved smaller problems. Although the Agents could keep writing new proofs, it was difficult to judge how many key steps had actually been solved and how far they were from the final goal.

Axiom had to readjust its strategy, splitting complex proofs into smaller and clearer tasks, and requiring Agents to explain how these small proofs combined step by step to ultimately yield the originally required conclusion.

AI digs up a 40-year-old account,

and adds a new proof

When the proof reached the deepest depths of the historical literature, the Agents discovered something more troublesome than task scheduling: the original mathematical papers could also be wrong.

Human mathematicians often omit familiar reasoning, but Lean requires every premise to be stated explicitly. According to Axiom's count, during the formalization process there were 34 literature deviations worthy of attention that needed to be handled, including typos, omitted conditions, and substantive issues that had to be rederived.

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 equation to an inequality could fix the lemma, but the later reasoning had relied on that equality. The team had to expand the scope of applicability of the preceding argument and rehandle the affected cases.

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

UGT is an important tool for the classification of finite simple groups. It helps mathematicians use a specific local structure within a group to infer what type the entire group may belong to. One of Walter's key arguments assumed by default that applying a certain operation to a specific family of groups would yield a related simple group that still belonged to the original family.

The Agent found a counterexample. Starting from PSL₂(49) and considering the involutions induced by its finite field automorphisms, the simple group components of the relevant centralizers would include PSL₂(7). But the latter happened not to belong to the family of groups specified by Walter, so the original closure assertion could not hold.

This did not overturn the conclusion of UGT, but it meant that when following this proof route, one step had to find another basis.

Axiom consulted group theory experts Richard Lyons and Ronald Solomon for this. Solomon's maximal 2-component theory, proposed in 1976, provided a key idea for a new route.

The Agent then constructed and formalized a new group theory result, "Preservation of simple tops," proving that under the required conditions, the relevant simple group structure can be preserved when comparing specific subgroups. It was written into a 35-page paper, "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 completed, Axiom's mathematicians found a shorter path in the first-generation proof method, which could reach the target conclusion without invoking this new theorem. However, the new theorem and its complete proof were still retained, becoming an additional mathematical outcome produced by this engineering effort.

The Unbalanced Group Theorem research that the Axiom team participated in completing included Theorem 2.3, "Preservation of simple tops," a new mathematical result obtained during this formalization process. Image source: the paper "The Unbalanced Group Theorem."

After 43.1 million lines of Lean,

what changed in mathematical proof?

Ultimately, Axiom uploaded the entire project to GitHub, making public approximately 43.1 million lines of Lean code. The final classification proposition in the repository expresses that every finite simple group is isomorphic to some already constructed group in the list.

The project claims that the final proof contains no sorry—in Lean, this is a placeholder for temporarily skipping an unfinished proof. The final result depends 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 actually relies on.

The final Lean code of the finite simple group classification theorem made public by Axiom. The final conclusion is obtained by invoking already formalized underlying proofs, backed by a proof engineering effort consisting of tens of millions of lines of Lean code. Image source: Axiom Math / GitHub.

The foundation of this work also includes existing formalization projects such as Mathlib, TauCeti, and Qiuzhen-CFSG, of which about 1.2 million lines came from Qiuzhen-CFSG. Research results accumulated by human mathematicians, early formalization infrastructure, and AI Agents that can work in parallel were placed into the same engineering workflow.

For subsequent mathematical research, a key change is that proofs can be continuously maintained. In the past, citing the finite simple group classification theorem might involve hundreds of papers; now, researchers can follow the formalized dependency chain to check exactly which definitions, conditions, and derivations were used.

The repository made public by Axiom labels the review status as team self-assessment. Next, external mathematicians can still check whether the formalized definitions accurately correspond to the original propositions and review the mathematical choices in this enormous project. But Lean has already provided another capability that was previously difficult to obtain: allowing the logical derivations of tens of millions of lines of proof to undergo unified, mechanized checking.

Looking back at these 24 days, what is most noteworthy is not how long the code written by AI is, but that it began to handle a large-scale research effort that previously relied heavily on human experts: decomposing tasks, tracking proofs, discovering errors in old literature, and participating in constructing new proofs when the old route did not work.

Mathematical knowledge accumulated over decades is changing from arguments scattered across papers into a structure that can be checked, reused, and further expanded by programs. What Axiom demonstrated this time is precisely a concrete attempt by AI to move from solving a single math problem toward participating in the construction of an entire mathematical theory.

"Special statement: The above content (including videos, pictures, and audio if any) is uploaded and published by users of the "Dafeng Hao," a self-media platform under Phoenix Net. This platform only provides information storage space services.

Notice: The content above (including the videos, pictures and audios if any) is uploaded and posted by the user of Dafeng Hao, which is a social media platform and merely provides information storage space services."