Axiom's multi-agent system formalizes the classification theorem of finite simple groups in 24 days

The largest mathematical proof in human history has now been formally verified by computer.

The Classification of Finite Simple Groups (CFSG) theorem has just been completely formalized by AI!

More than a hundred of the world's top mathematicians spent over half a century and wrote a 15,000-page "mathematical tome," and a multi-agent system developed by the startup team Axiom ran it all through in just 24 days.

What is even more mind-boggling is that the AI built the first Lean codebase in human history to exceed 40 million lines.

Measured by lines of code, this is now the largest open-source software project in history. Its scale exceeds that of the Linux kernel, Chromium, Firefox, LLVM, GCC, FFmpeg, and others.

It even caught human flaws in the original proof and personally proved new mathematical theorems to patch them!

The renowned mathematician Ken Ono posted an emotional message mourning his mathematician father, who passed away in January of this year.

He recalled the years of his childhood when his father introduced him to the giants of group theory, and when he witnessed human-machine collaboration cross this historic finish line, this master of mathematics could not hold back his tears on the spot.

Mathematics' "Periodic Table of Symmetry": The Enormous Theorem

In the mathematical world, this theorem has a resounding nickname—"The Enormous Theorem."

Before this, no one in the world had ever been able to read all of its proofs completely from beginning to end.

For example, viewing the Rubik's Cube through graph theory, each state is a vertex, and each move is an edge in this enormous graph.

This animation shows how permutations traverse 43 quintillion configurations and finally reach the solution.

And all finite groups can, like chemical molecules being broken down into atoms, be decomposed into indivisible "basic building blocks"—these are the finite simple groups.

The greatness of the classification theorem lies in the fact that it provides a "periodic table of elements" for symmetry throughout the entire universe.

It explicitly declares:

Every finite simple group either belongs to a cyclic group of prime order, or to an alternating group on at least 5 symbols, or to one of the 16 infinite families of groups of Lie type, or else to one of the 26 extremely special, unclassifiable "sporadic groups."

Among these 26 sporadic groups, the largest one is reverently called by mathematicians the "Monster Group."

By the way, in 1998, Richard Borcherds was awarded the Fields Medal for proving the famous "Monstrous Moonshine" conjecture. This conjecture revealed a shocking connection in mathematics: the largest sporadic simple group, the "Monster Group," actually has a profound mathematical connection with modular functions in number theory.

In 2007, the physics giant Edward Witten even proposed that this theory involving the Monster Group might be used to describe gravity in a simplified universe, to encode the distribution of quantum states of black holes at different energy levels, and thereby calculate the entropy of black holes!

Starting in the 1950s, in order to prove the Enormous Theorem, about 100 mathematicians pieced together a proof 15,000 pages long across more than 500 academic papers—roughly 14 copies of Dream of the Red Chamber.

It was so vast and scattered that when the mathematician Gorenstein announced in 1983 that the proof was complete, a huge gap had actually been left out, and it was not filled until 2004 by Aschbacher and Smith with a 1,221-page paper.

Because the proof is simply too long, humans are extremely prone to error. As Aschbacher said: "It is impossible to write a very long and complicated argument without making mistakes."

AI Sets Out: 24 Days, Doing Half a Century of Human Work

Facing this 15,000-page "Mount Everest of mathematics," the Axiom team did not choose traditional brute-force computation, but instead deployed a multi-agent swarm—AxiomProver.

Translating human natural-language proofs into Lean code (that is, "formalization") is equivalent to making an impartial machine inspect every punctuation mark on those 15,000 pages with a magnifying glass.

On October 1, 2026, the Axiom team typed the launch command in a Slack channel.

Human engineers and mathematicians broke the enormous "Enormous" into 108 milestones and about 380 small tasks, generating a huge "proof map."

On October 2, the first batch of AI "swarms" officially went online.

This group of AI agents began to divide the work and collaborate like a well-trained army. The lead AI was responsible for breaking down highly difficult arguments, while other AIs frantically searched existing results or buried themselves in writing Lean code. If an AI encountered a prerequisite that had not yet been proved, it would automatically outsource the task to another AI. All results would converge into a shared codebase.

The whole process was not smooth sailing. Because the AI wrote code so fast, the Lean system even hit a computing bottleneck when rechecking dependencies.

Axiom's engineers had to temporarily refactor the underlying engineering infrastructure and develop a distributed caching system before they could barely keep up with the AI's terrifying output speed.

On October 10, a message popped up in the Slack channel that set everyone ablaze:

We proved that the Monster group is simple.

Just 24 days!

Over 24 days and nights, this tireless swarm of AI agents produced an astonishing 43.1 million lines of Lean code, building the largest Lean codebase currently in existence.

Human wisdom was subjected to the machine's ruthless scrutiny—and logical gaps were found within it!

An epic reversal: AI uncovers a human master's "fatal bug" and fixes it by hand

A formal proof requires that every step have explicit logical support.

In the process of line-by-line scanning and forced reasoning, the AI agents recorded hundreds of anomalies. Most of these were human typos, table errors, or missing preconditions, but 34 were major logical deviations!

And the most perilous and central "bug" of them all lay in the crucial Unbalanced Group Theorem (UGT).

UGT is an extremely critical link in the entire classification theorem; its role is to "see the whole through the parts"—by studying the subgroup structure of a group, it infers the true nature of the entire large group.

The Axiom team initially chose an authoritative paper published by John Walter in 1986 as the basis for formalization.

The AI found that a key closure assertion in Walter's proof was logically untenable.

The AI not only pointed out the error but also provided a clear counterexample: PSL₂(49). In this counterexample, one operation produces a group that is explicitly excluded from the target family (because 7 is a Mersenne prime).

Humanity's proud proof broke its chain at this moment.

A logical edifice 15,000 pages long stood in danger of collapsing at any moment.

What to do? Borrowing a "second-generation proof" written by later scholars would not only introduce a massive number of entirely new dependencies but also render the efforts of these 24 days futile.

At this moment, the pinnacle of human-machine collaboration unfolded.

The Axiom team urgently contacted living fossils who had participated in the original CFSG work—the titans of group theory Richard Lyons and Ronald Solomon.

After hearing about the gap the AI had discovered, the intuition of the human masters and the computational power of the AI resonated perfectly. Based on a theory proposed by Solomon in 1976, the human mathematicians conceived a new proof route.

Subsequently, AxiomProver (the AI system) took the field in person and, following the new approach, rigorously proved an entirely new group-theoretic result—Preservation of simple tops.

This new theorem, proved under AI leadership, fit like a perfectly tailored patch, precisely filling the hole left by the human masters back then and successfully deriving the form of UGT required by the classification theorem!

The theorem still holds, but the proof no longer belongs entirely to humans.

This inevitably brings to mind a similar episode in the history of mathematics: Vladimir Voevodsky, winner of the 2002 Fields Medal, discovered that his own proof was wrong—and could not be salvaged.

In 1999–2000, while lecturing at the Institute for Advanced Study in Princeton, he discovered that a key lemma from his early work was flawed, and the original proposition could not be rescued as it stood.

In 2013 he further confirmed that another result from 1989 was also wrong—a counterexample had been raised as early as 1998.

He no longer believed that humans could reliably check complex proofs, and turned to Coq, homotopy type theory, and univalent foundations: letting computers verify mathematics.

On the road to mathematical truth, humans, with flesh and blood and finite brains, undertook a tragic and heroic expedition lasting nearly two hundred years.

Today, humanity has a new partner, together exploring the vast sea of stars in the realm of knowledge.

References:

This article comes from the WeChat public account "Xinzhiyuan" (ID: AI_era), author: ASI Revelation, published by 36Kr with authorization.