The largest proof project in mathematical history has now been formally verified by computer, according to a report citing Axiom and related source material.
Axiom said its multi-agent system, AxiomProver, has fully formalized the Classification of Finite Simple Groups, or CFSG. The source article describes CFSG as a decades-long effort built by about 100 mathematicians from the 1950s onward across more than 500 papers and roughly 15,000 pages, then converted into Lean code in 24 days.
A theorem known as “The Enormous Theorem”
In mathematics, the Classification of Finite Simple Groups has long carried the nickname “The Enormous Theorem.” The article says that before this effort, no single person had read every proof in full from beginning to end.
Groups are presented in the report as the language of symmetry. Finite groups, in that framing, can be broken into irreducible building blocks in the same way molecules can be decomposed into atoms. Those building blocks are finite simple groups, and the classification theorem gives a complete list of them.
The article lists four categories: cyclic groups of prime order, alternating groups on at least five symbols, groups of Lie type in 16 infinite families, and 26 exceptional sporadic groups. The largest sporadic group is the Monster Group.
The report also points to later links around the Monster. It notes that Richard Borcherds won the Fields Medal in 1998 for proving Monstrous Moonshine, and that Edward Witten proposed in 2007 that theory involving the Monster could be used in a simplified universe to describe gravity and encode the distribution of black-hole quantum states across energy levels for entropy calculations.
The proof corpus took shape over decades. The source says about 100 mathematicians assembled it in more than 500 academic papers, producing around 15,000 pages in total. It also says the proof was not actually complete when Daniel Gorenstein declared it finished in 1983. A major gap remained and was only filled in 2004 by Michael Aschbacher and Stephen Smith in a 1,221-page paper.
The article quotes Aschbacher as saying, “It is impossible to write a very long and complicated argument without making mistakes.”
AxiomProver generated 43.10 million lines of Lean code
Rather than relying on brute-force computation, Axiom used AxiomProver to translate natural-language mathematics into Lean, the formal proof language named in the report.
The timeline in the article starts on Oct. 1, 2026, when the team issued a launch command in a Slack channel. Human engineers and mathematicians broke the project into 108 milestones and about 380 smaller tasks, creating what the report calls a proof map. The first AI “swarm” went online on Oct. 2.
The agents split work across decomposition, search, and code writing. When one agent hit an unproven prerequisite, the task could be handed off to another agent. Results were merged into a shared codebase.
The process also ran into infrastructure limits. The article says Lean hit compute bottlenecks while rechecking dependencies because the AI was producing code too quickly. Axiom engineers then rebuilt parts of the underlying infrastructure and added a distributed caching system to keep up.
On Oct. 10, the Slack channel produced a message the report highlights: “We proved the Monster is simple.” The article says the AI not only identified the Monster from structural information but also fully formalized its existence in code.
After 24 days, AxiomProver had produced 43.10 million lines of Lean code. The report describes this as the largest Lean codebase so far. By line count, it also says the repository is larger than the Linux kernel, Chromium, Firefox, LLVM, GCC, and FFmpeg.
Hundreds of anomalies surfaced during formalization
Formal proof systems require every step to be explicit. The article contrasts that with common shortcuts in mathematical writing, where authors may skip steps with phrases equivalent to “obvious,” “similarly,” or “left to the reader.”
According to the report, AxiomProver logged hundreds of anomalies while scanning the proof line by line and forcing each inference to be justified. Most were described as typos, table mistakes, or omitted assumptions. Another 34 were labeled major logical deviations.
The most serious issue appeared in the Unbalanced Group Theorem, or UGT, which the article describes as a central part of the overall classification because it infers the structure of a larger group from the structure of its subgroups.
Axiom initially used a 1986 paper by John Walter as the basis for formalization. But while translating that argument, the AI flagged a key closure claim as logically invalid.
The system also produced a concrete counterexample: PSL₂(49). In the article’s description, one operation in that case generates a group explicitly excluded from the target family because 7 is a Mersenne prime. The report presents that moment as a break in the chain of reasoning for the broader 15,000-page structure.
Lyons and Solomon joined the repair effort
The article says Axiom did not switch to a later “second-generation proof” because doing so would have introduced a large number of new dependencies and risked undoing the previous 24 days of work.
Instead, the team contacted Richard Lyons and Ronald Solomon, both described in the report as veterans of the original CFSG effort. After reviewing the flaw found by the AI, the mathematicians developed a new route based on theory Solomon had proposed in 1976.
AxiomProver then proved a new group-theoretic result called Preservation of simple tops. The article describes it as a custom patch that filled the hole in the human proof and recovered the form of UGT needed for the classification theorem.
In that telling, the theorem still stands, but the proof is no longer entirely human. The report frames this as the first time AI has gone beyond checking work in top-level pure mathematics and taken part in discovering a new theorem and repairing a core gap.
Ken Ono reflected on the milestone
The article also cites a post by mathematician Ken Ono, who wrote about the development while mourning his father, a mathematician who died in January. Ono recalled being introduced in childhood to major figures in group theory through his father and, according to the report, broke down in tears while witnessing the human-machine collaboration reach this point.
The piece closes by recalling another episode from mathematical history. It says Fields Medalist Vladimir Voevodsky discovered that one of his own proofs was wrong and could not be repaired. During lectures at the Institute for Advanced Study in Princeton in 1999 and 2000, he found a key earlier lemma was flawed, and in 2013 he confirmed another 1989 result was also wrong, with a counterexample having already appeared in 1998. The article says that experience pushed him toward Coq, homotopy type theory, and univalent foundations as ways to let computers check mathematics.
The source article cites Ken Ono’s post on X and Axiom’s research page, “The Enormous Theorem Formalized.” It also says the Chinese article was republished from the WeChat account “新智元,” credited to “ASI启示录.”
