The largest proof project in modern mathematics just got its first serious machine audit. In seven months, an AI-driven workflow called FormaTheoria wrote more than 994,000 lines of Lean code to formalize four cornerstone theorems of the Classification of Finite Simple Groups (CFSG) — the sprawling proof effort that runs to roughly 20,000 pages across hundreds of papers, built by hundreds of mathematicians over decades.
The four theorems — the Feit–Thompson odd order theorem, the Glauberman Z* theorem, the Brauer–Suzuki theorem, and the Bender–Suzuki theorem — form a connected chain at the heart of the classification. Here is the scale check: a previous formalization of just the Feit–Thompson theorem, done in the Rocq (Coq) proof assistant, took about 15 people six years. FormaTheoria completed that body of work in seven months and extended it further.
That is the headline. The more interesting story is how the system did it, because the engineering generalizes far beyond mathematics.
Not an AI that solves prepared problems
Most AI math systems receive a clean problem statement with definitions and tools already assembled, then search for a proof. FormaTheoria works differently. It starts from raw, messy literature and must first rebuild the mathematical foundations underneath the theorem — reading books, resolving dependencies, reconciling notations — before constructing the formal proof and submitting every step to the Lean proof assistant. The project was initiated under Shing-Tung Yau's advocacy, with students from Tsinghua's Qiuzhen College plus researchers from the Yau Mathematical Sciences Center, the Institute for AI Industry Research, and the University of Warwick.
The authors describe four hard problems, each with an engineering answer:
- You do not know how much reading is required. A citation leads to a paper, which leads to more prerequisites. The project started with 3 principal sources and discovered 12 more mid-proof; 65.6% of all pages consulted were added during the proof itself. The system's answer: when a missing prerequisite appears, pause the proof, formalize the dependency, and return to the task. Every verified result is archived in a shared knowledge base for later theorems to reuse.
- Definitions do not compose across papers. Two authors can define the "same" concept differently — mathematically equivalent in prose, incompatible once written in Lean. The system builds explicit translation bridges between sources and protects already-verified statements from collateral damage during repairs.
- Code that passes Lean can still misread the original. Lean checks that a proof is self-consistent and that the conclusion follows from the premises. It does not check whether the conclusion faithfully represents the paper. The AI might drop a condition, blur "all" vs. "exists," or silently modify a conclusion. The answer is a dedicated independent review stage: a translator component writes the Lean statement, and a reviewer component re-checks it line by line against the source. Of the 14 literature sections analyzed, 11 first-draft translations were sent back for revision. This second gate is what separates "machine-verified" from "machine-misread."
- The original literature is sometimes simply wrong. Older papers carry typos, missing hypotheses, and ambiguous phrasing. The system caught two incompatible definitions of "type I maximal subgroup" across sources and bridged them using the Schur–Zassenhaus theorem; it flagged a lemma in Péterfalvi missing its odd-order precondition; it found a theorem in Huppert with a wrong divisibility condition, produced a counterexample, and escalated the question to human mathematicians, who confirmed the correct condition. Even a plain typo survived in both reference books — the object H written as M throughout.
Long-horizon engineering matters as much as the reasoning itself. A constantly updated "proof map" breaks hard goals into lemmas, merges successful results upward into the main theorems, and logs failed paths so the system does not repeatedly walk into the same dead ends. Dependency-aware parallelism computes shared prerequisites once for every consumer (a 4.2× speedup on the tested tasks). The longest single agent run lasted 9.17 days, during which the system performed 606 passes of memory compression while keeping the current goal, completed results, and open questions alive.
The final numbers: 30,298 math statements and 186,187 dependency edges in the proof network, with the longest dependency chain 458 layers deep. Counting Lean's standard library, the network grows to 74,922 statements and more than 1.44 million dependencies.
The useful frame: math papers are an undocumented legacy codebase
CFSG is 20,000 pages of prose written by hundreds of authors across decades, with conventions that "readers in the field will know." No compiler ever checked any of it. Errors hide in plain sight because competent readers silently correct them as they read.
Formal verification is the compiler mathematics never had. Every definition, every condition, every inference must be explicit. The AI's job was not "writing a proof" — it was rebuilding the entire dependency graph of a 20,000-page system and making it type-check. The verification is the visible result; the real asset is the reconstructed, auditable infrastructure underneath.
For anyone who has worked with legacy systems, the analogy is precise. Math papers are a codebase without tests that everyone is afraid to refactor. The proof map is an issue tracker. The reviewer pass is a code review. Escalating to mathematicians is an incident process. The novelty is not the management — it is that an AI agent now runs the whole operation.
Why this matters beyond math
First, the capability boundary moves. AI is no longer limited to solving prepared, isolated problems. It can now maintain and extend a large, long-horizon knowledge infrastructure — running for days, compressing context, tracking dependencies across dozens of sources, and keeping a multi-week thread coherent. That is an agent capability, and it generalizes to any domain with large, interconnected bodies of knowledge.
Second, the verification pattern is a template for trustworthy AI. Note the three layers: a checker that proves internal consistency (Lean), an independent reviewer that checks fidelity against the source of truth, and a human escalation path when evidence is insufficient. Enterprise AI that generates code, contracts, or scientific claims needs exactly this split. The generator can be fluent; the verifier must be adversarial; the human owns the judgment call.
Third, verified mathematics becomes a reusable asset. The formalized network will serve as infrastructure for future theorems, the way a well-tested library is infrastructure for future software. Once search, explanation, and visualization tools are attached, researchers will query this network instead of re-deriving it by hand.
Fourth, this is the working version of human–machine collaboration. Humans decide which problems are worth solving and make the key judgments; AI performs the large-scale search and derivation; formal systems guarantee that every accepted step can be re-checked. When a proof is too large for any individual to re-read, that division of labor is not a choice — it is the only option.
What you can take away
- If you build long-running agents, manage them like FormaTheoria: a persistent progress map, logged failed paths, compressed memory, and shared dependencies computed exactly once.
- If you ship AI-generated code or claims, add an independent fidelity check against your source of truth. Passing the checker is not the same as being faithful — 11 of 14 first drafts were rejected by review in this project.
- Do not treat "machine verified" as a synonym for "machine understood." Verification tooling guarantees internal consistency, not correspondence to intent. You need both layers, or you get rigor without truth.
Paper: arXiv:2608.10894 · Code: github.com/Qiuzhen-CFSG/CFSG
