Dozens of agents spent 24 days challenging a massive project in the mathematics community, and even unearthed a loophole that had gone unnoticed 40 years ago.
Over 100 top mathematicians spent decades writing 15,000 pages of proofs.
Now, AI has used 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 computers.
Even more strikingly, while AI was reviewing the proofs left by these mathematicians, it also spotted a demonstration loophole that had existed for nearly 40 years.
This is not an Olympiad math problem, nor a dozens-of-pages mathematical paper, but the Classification 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 had been completed, but later people found that there were still parts that had not been filled in. It was not until 2004 that mathematicians used another 1221 pages of proofs to fill a key gap.
On October 26, Axiom Math, an AI mathematics company, announced that dozens of AI Agents organized by human mathematicians and engineers completed the Lean formalization of this Enormous Theorem within 24 days, generating approximately 43.1 million lines of code and 2.05 million formal statements, and delivered the first computer-checked proof covering the entire Classification of Finite Simple Groups.
The mathematical reasoning originally scattered in more than 500 papers has now been organized into a formal system that can be checked step by step. What is more surprising is that in this process, the Agents not only found errors in historical papers, but also participated in constructing a new group theory result.
The formalization project of the Classification of Finite Simple Groups publicly released by Axiom includes about 43.1 million lines of Lean code, 2.05 million statements, 100 milestones, and involves 715 references. Source: Axiom Math official website.
What exactly has the mathematical community spent decades proving?
To understand the difficulty of this work, we have to start with "symmetry".
Take a square piece of paper: after rotating 90 degrees, its shape completely coincides with the original one; the same applies to 180-degree and 270-degree rotations. 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 basic parts. Just as integers can be decomposed into prime factors, these indivisible "elementary particles" are called finite simple groups.
The Classification of Finite Simple Groups aims to answer a seemingly simple question: what are all these elementary particles exactly?
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". Among them, the largest "Monster Group" has about 8×10^53 elements. Proving its existence alone was once a major achievement in the mathematical community.
Schematic diagram of the relationship between some "sporadic simple groups". The M at the top represents the largest sporadic simple group "Monster Group", and other nodes represent different sporadic simple groups.
Identifying these groups only completed half of the work. The real difficulty lies in proving that: apart from the types in the list, there cannot be a 27th sporadic simple group, nor any new type that has not been discovered yet.
In 1963, Walter Feit and John Thompson published a 255-page paper proving that all non-commutative finite simple groups have even order, which opened a breakthrough for subsequent classification. In 1972, Gorenstein put forward a 16-step research plan; in 1983, he announced the completion of classification. The remaining proof gap for quasi-thin groups was not filled until 2004 by Michael Aschbacher and Stephen Smith, and further corrections were made in 2008.
The huge proof is like a relationship network spanning decades: a theorem in one paper cites a theorem from another paper, which in turn relies on lemmas from even earlier works. Many steps also omit conditions that the authors consider obvious. Even if each paper seems reasonable on its own, it is difficult for one person to check every connection in the entire system.
What Axiom is doing this time is to convert all these connections into proofs that computers can verify.
The 24-day Agent project was almost dragged down by "correct proofs"
This is not a process where a large model reads 15,000 pages and then spits out tens of millions of lines of code at one go.
On October 1, Axiom opened a dedicated Slack channel, sorted out a proof roadmap with 108 milestones and about 380 specific tasks using the existing Lean base library and mathematical literature. On October 2, the first batch of Agents began to claim tasks via GitHub Issues.
Some Agents are responsible for decomposing theorems, some search for existing results, some generate Lean proofs, and others review propositions and integrate codes. When encountering unfinished pre-theorems, Agents can continue to assign tasks to other Agents. Human mathematicians handle key obstacles, and engineers are responsible for coordinating these continuously working systems.
These Agents run in coordination with AxiomProver, a mathematical proof system independently developed by Axiom. The project adopts a multi-model combination that is continuously adjusted, but the specific list of underlying models is not disclosed. Compared with relying on a single model to complete reasoning, this system places more emphasis on task decomposition, proof generation and collaborative verification between different Agents.
The Treemap of the Axiom formalization project for the Classification of Finite Simple Groups, showing the scale of Lean statements and codes in different mathematical modules. Source: Axiom Math.
Shortly after the project started, a tricky problem emerged: an Agent could prove a mathematical proposition, but it might not prove the exact one the project really needed.
For example, the original requirement was to prove that a bridge can safely pass heavy trucks, but the Agent first added a condition: "Assume that the bridge piers are strong enough". With this premise, it successfully proved that the truck can pass, and even Lean recognized the entire derivation.
But the problem is, whether the bridge piers are strong enough has not been proved at all.
Similar problems occurred repeatedly in the early stage of the project. Some seemingly completed mathematical tasks actually quietly introduced unproven premises. Axiom had to delete tens of thousands of lines of code built on these assumptions and rearrange the work.
As the code base expanded, Lean's checking speed could not keep up with the output of Agents. Modifying a basic theorem might force all codes that depend on it to be rechecked. To this end, engineers introduced shared build cache and parallel verification mechanisms to allow different Agents to reuse the confirmed results as much as possible.
On October 10, good news came from the team's Slack channel: "WE PROVED MONSTER IS SIMPLE." The Agent had completed the formalization of the simplicity of the Monster Group, and formalized its existence through the Griess algebra.
But three days later, the project progress suddenly slowed down. On October 13, although dozens of Agents were still generating codes non-stop, the team only completed one phased proof task the whole day.
The problem lay in task decomposition. The remaining mathematical problems were too complex, and there were many unsolved small problems hidden under one big problem. Although the Agents could keep writing new proofs, it was difficult for them to judge how many key steps had been solved and how far they were from the final goal.
Axiom had to readjust its strategy, split complex proofs into smaller and clearer tasks, and require Agents to explain how these small proofs are combined step by step to finally get the originally required conclusion.
AI dug up a 40-year-old old issue and even supplemented a new proof
When the proof went deep into the most ancient parts of historical literature, the Agents discovered something more troublesome than task scheduling: the original mathematical papers might also be wrong.
Human mathematicians often omit familiar reasoning, but Lean requires every premise to be written clearly. According to Axiom's statistics, there are 34 notable literature deviations to be handled during the formalization process, including clerical errors, missing conditions, and substantive problems that must be re-derived.
One example appears in Aschbacher and Smith's work on "quasi-thin groups". A lemma in the original text asserts that two quantities are equal, but the Agent found a counterexample with the group SL₂(5): one quantity is 1, while the equation requires it to be 2. Changing the equality to an inequality can correct the lemma, but the subsequent reasoning once relied on that equal sign. The team had to expand the scope of application of the previous section of argument and reprocess the affected situations.
A bigger 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 infer what type the entire group may belong to by using a specific local structure inside a group. One of Walter's key inferences defaults that after a certain operation is performed on a specific group family, the related simple groups obtained still belong to the original group family.
The Agent found a counterexample. Starting from PSL₂(49), consider the involution induced by its finite field automorphism, the simple group component of the related centralizer will appear as PSL₂(7). But the latter does not belong to the group family limited by Walter, and the original closure assertion cannot hold.
This does not overturn the conclusion of UGT, but it means that when following this proof route, one step must 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 key ideas for the new route.
The Agent then constructed and formalized a new group theory result "Preservation of simple tops", which proves 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 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 are still retained, becoming an additional mathematical output of this project.
The research on the Unbalanced Group Theorem completed by the Axiom team, in which Theorem 2.3 "Preservation of simple tops" is a new mathematical result obtained during this formalization process. Source: the paper *The Unbalanced Group Theorem*.
After 43.1 million lines of Lean code, what changes have taken place in mathematical proofs?
Finally, Axiom uploaded the entire project to GitHub and made about 43.1 million lines of Lean code public. The final classification proposition in the repository expresses that every finite simple group is isomorphic to some group that has been constructed in the list.
The project statement finally proves that the proof contains no sorry — in Lean, it is a placeholder that temporarily skips unfinished proofs. The final result only depends on standard axioms and can be checked step by step by the Lean kernel. Axiom also provides an interactive proof dependency graph, allowing researchers to track which pre-theorems a conclusion relies on.
The final Lean code of the Classification of Finite Simple Groups publicly released by Axiom. The final conclusion is obtained by calling the formalized underlying proofs, behind which is a proof project composed 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, of which about 1.2 million lines come from Qiuzhen-CFSG. The research results accumulated by human mathematicians, early formalization infrastructure, and AI Agents that can work in parallel are integrated into the same set of engineering processes.
For subsequent mathematical research, a key change is that proofs can be continuously maintained. In the past, citing the Classification of Finite Simple Groups might involve hundreds of papers; now, researchers can follow the formalized dependency chain to check which specific definitions, conditions and derivations are used.
Axiom marks the review status of the public repository 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 huge project. But Lean has provided another previously inaccessible capability: allowing the logical derivation of tens of millions of lines of proofs to undergo unified, mechanized inspection.
Looking back at these 24 days, the most noteworthy thing is not how long the code written by AI is, but that it has begun to deal with a large-scale research work that was highly dependent on human experts in the past: decomposing tasks, tracking proofs, discovering errors in old literature, and participating in constructing new proofs when the old route does not work.
Decades of accumulated mathematical knowledge is being transformed from arguments scattered in papers into structures that can be checked, reused and continuously expanded by programs. What Axiom demonstrated this time is a specific attempt for AI to move from solving a single math problem to participating in the construction of a whole set of mathematical theories.