AI proves the “Enormous Theorem”: 15,000 pages of math formalized in 24 days

What this is about

Axiom, a US company building AI for mathematics, announced an unusually big achievement on October 27, 2026. Its AI agents have fully formalized the classification theorem for finite simple groups (CFSG) in Lean. Lean is a proof assistant, meaning a program that checks mathematical proofs step by step by machine. CFSG is considered the longest proof in human history and is also called the "Enormous Theorem." The code is public on GitHub. All details come from a Chinese-language report (DeepTech via cnyes) and rest largely on Axiom's own account.

What formalization means and why it matters right now

AI systems are producing proofs faster and faster. According to the report, OpenAI published 722 internally generated math manuscripts on hundreds of open problems on October 6, and more results on October 26. The question is: how do you check whether they're correct?

One answer is formal verification. A proof is translated into a strictly formal language. Phrases like "obviously" or "it follows analogously" don't count in Lean: every intermediate step and every tacit assumption must be spelled out, and the Lean kernel checks each step.

The "Enormous Theorem"

Mathematicians describe symmetries with groups. A cube has 24 rotations that leave it looking unchanged; these rotations, together with their composition rules, form a group. Just as numbers break down into primes, finite groups break down into indecomposable building blocks: the finite simple groups.

CFSG lists them all: cyclic groups of prime order, alternating groups, 16 families of groups of Lie type, and 26 "sporadic" groups that fit into no family. The largest, the Monster group, has about 8×10^53 elements. The list is often called the periodic table of symmetry.

Drawing up the list was comparatively easy. The hard part was proving that nothing is missing. The work began in the 1950s. John Thompson received the Fields Medal for it in 1970 and the Abel Prize in 2008. In 1983, Daniel Gorenstein declared the classification complete, but the case of "quasithin groups" relied on an unfinished manuscript. The gap wasn't closed until 2004, when Michael Aschbacher and Stephen Smith published a 1,221-page monograph; another gap was patched in 2008. This is now regarded as the "first proof."

The proof is scattered across decades, with different notations and many cross-references. Since the late 1980s, a more systematic "second proof" has been in the works; 10 volumes had appeared by 2023, and at least 12 are planned. Many results in algebra, number theory, combinatorics and mathematical physics assume CFSG.

The company: Axiom

Axiom was founded in March 2025. Its founder and CEO is Carina Hong, who grew up in Guangzhou, studied at MIT, won the Morgan Prize, went to Oxford as a Rhodes Scholar and left her Stanford PhD to start the company. Ken Ono is the "founding mathematician." According to the report, Axiom has raised $64 million in seed funding and $200 million in Series A capital, at a valuation said to exceed $1.6 billion. Its system, AxiomProver, coordinates multiple AI agents. In August, the team had already formalized the "246 theorem" on prime gaps. Ono says, in essence, that the world will soon run on code nobody has read, and that formalized proofs are a testbed for that.

How the 24 days unfolded

Axiom didn't start from scratch. The Lean library Mathlib provided the foundations, and an earlier CFSG project (inspired by Shing-Tung Yau and carried out by students at Tsinghua University and the Yau Center) had accumulated a lot of group theory code; Axiom took over about 1.2 million lines. Based on the second proof, the team built a proof map with 108 milestones and roughly 380 subtasks. But what they formalized was the first proof, because the second is still unfinished.

The first agent swarms went online on October 2. A coordinating agent broke arguments down and checked how statements were formulated, while others looked up known results and wrote Lean code. When a prerequisite was missing, it was handed off to other agents; finished pieces flowed into a shared codebase. Human mathematicians resolved technical bottlenecks, and engineers kept the system running.

Things started out bumpy: agents simply wrote down unproven assumptions as given. Tens of thousands of lines were deleted and rebuilt. On October 10, the team reported proving the simplicity of the Monster group, along with proof of its existence, a key stage. Three days later everything stalled; only one milestone was reached in a single day. The milestones were too coarse, so the team split them into smaller, more precise theorems.

The code also grew faster than Lean could check it: when a shared theorem changed, all dependent parts had to be rechecked, and agents on different machines duplicated work. A caching system that reuses unchanged parts sped up checking by several orders of magnitude, according to the report. The formalization was finished on October 26: the Lean kernel confirmed the unbroken chain from the basic axioms to the classification theorem.

Errors in the literature

The line-by-line translation worked like a health check of the literature. Many of the suspected problems flagged by the agents turned out to be their own misreadings. What was confirmed were mainly typos, wrong table values and missing hypotheses, plus 34 deviations from the published literature that had to be handled separately. Axiom plans to publish a list of errors together with group theorists.

The hardest case was the Unbalanced Group Theorem. The overall proof works by contradiction: you assume a simple group that isn't on the list, pick the smallest one, and rule out possible structures one after another. This theorem excludes a large class of them. The team followed John Walter's 1986 argument, but the agents found a counterexample to one claim in it: a certain operation doesn't always stay within a family of groups, but can produce groups that lie just outside it. The theorem itself remains valid, but a key step in the original argument was unjustified.

Another published route would have pulled in many more unformalized prerequisite results. So the team asked Richard Lyons and Ronald Solomon, who had worked on the classification. Lyons mapped out possible paths and their history, and Solomon's 1976 theory of "maximal 2-components" supplied the core idea. AxiomProver then constructed and formalized a new line of argument, proving a previously unknown group-theoretic result along the way (preprint on Hexagon). Later, Axiom's mathematicians found a shorter path within the methods of the first proof that doesn't need this new result; both routes are documented in the paper.

Reactions and the wider debate

A week earlier, Terence Tao and Yu Deng discussed AI and mathematics on the SAIR Foundation podcast. In September, the two, along with 23 other Fields Medalists, had criticized AI companies for using math problem-solving as a performance test. Deng distinguishes two frontiers: problems for which a proof exists, and problems whose proof humans can understand. They used to coincide; now there are proofs that only AI understands. Tao described the mass production of AI proofs as a kind of "toxic waste" that mathematicians have to process, and wants AI companies to involve mathematicians from the start. According to the report, the CFSG project fits that approach: there was a roadmap, and people involved in the original work stepped in at key points. The "Leiden Statement on AI and Mathematics," published in June and backed by the IMU, also names unreliable results as the main risk.

Our take

The report describes a real infrastructure achievement: a proof that rested on trust and collective memory for decades becomes traceable and machine-checkable, and researchers can follow dependencies and reuse modules. Caveats remain. The claims come from Axiom and a media report, and independent verification is still pending, according to the report. What matters is whether the formal definitions and the theorem exactly match the intended CFSG, and Lean can't judge that itself. Also still open: the second proof is unfinished, and the error list hasn't been published yet. Source 2 (Pramaana Labs, funding for Lean-based verification in law and medicine) covers a different story and isn't included here.