Axiom formalizes the Stacks Project in Lean: 16 million lines, split into human-reviewed and AI-only tiers

A week after its Lean proof of the classification of finite simple groups, Axiom Math has released a Lean 4 formalization of the Stacks Project, the roughly 7,500-page open-source reference on algebraic geometry started by Columbia mathematician Johan de Jong in 2005. In its November 4 post, The Stacks Project, formalized in Lean, Axiom puts it at about 16 million lines of Lean and calls it "the largest integrated, reusable library of formalized mathematics ever built." The code is on GitHub as AxiomMath/Stacks under Apache 2.0, built on Mathlib, and the repository's metadata lists Kenny Lau, Brian Nugent, Ashvin A. Swaminathan and Yunzhou Xie as authors and maintainers.

A library, not a theorem

The CFSG project was organized around one landmark result. The Stacks Project is the opposite: thousands of interlocking definitions and lemmas, each with a permanent four-character tag, meant to be cited by other proofs. Axiom kept that structure. Every declaration that formalizes a tag carries an attribute such as @[stacks 00DS], tags already covered by Mathlib are registered on the Mathlib declaration instead, and declarations are also tagged with the items of Grothendieck's EGA and SGA they prove. The companion site, stacks.axiommath.ai, shows each tag's Lean code next to the original text, with a browsable dependency graph.

The point is reuse. Someone formalizing a new result about families of curves, human or agent, can import Stacks instead of rebuilding schemes and coherent cohomology first. Axiom's argument is that modern algebraic geometry was out of reach for quick formalization, because a single proof can rest on a long chain of commutative algebra, sheaves, cohomology and stacks that didn't exist in Lean.

How much of it has a human looked at

The repository is more precise than the announcement. According to its README, Axiom has "formalized every tag of the Stacks Project with formalizable content", with no sorry, no native_decide, and only Lean's three standard axioms. Exercises and obsolete chapters are out of scope, and unformalized examples, exercises and remarks are left as tasks for contributors.

The library has two tiers. StacksCore holds code a person has checked against the Stacks Project and brought up to Mathlib standards. StacksFrontier holds code written by AI agents (the repository credits AxiomProver, Axiom's in-house prover, working with human formalizers) that builds and passes the kernel but hasn't had that review. Both are kernel-checked, so the proofs are not in doubt. What review checks is whether each Lean statement actually says what the Stacks text says, and whether the definitions are ones a human would want to build on. Axiom says faithfulness was enforced automatically through multi-agent audits and semantic cross-checks, plus targeted audits of foundational definitions and major theorems. Neither the post nor the README gives the split between the two tiers.

The build is also not small: the library has about 63,000 modules, and the README warns that a full build takes "a long time and a lot of memory" until a cache for compiled Stacks modules is available.

Errors in the text

As with CFSG, the formalization turned up problems in the source. Axiom says its system found "dozens" of statements in the Stacks Project that needed local fixes: missing hypotheses, edge cases in positive characteristic and claims that don't hold in the stated generality. Agents constructed counterexamples, formalized corrected versions, and where a false lemma left a gap in a deeper proof, found another route through the literature to the main result. Axiom doesn't list them in the post; it says the counterexamples can be inspected on the site.

These won't go upstream automatically. On October 21 de Jong asked that AI-generated comments and pull requests not be submitted directly to the Stacks Project repository for now. Axiom says it respects that and keeps its formalization and corrections in its own repository. So for the moment, the human-maintained Stacks Project and its Lean twin can disagree, and it is up to de Jong's contributors whether to take the corrections.

What to watch

Two numbers would make the claim easier to judge: how much of the library is in the reviewed StacksCore tier, and the full list of statements Axiom says were wrong. Mathlib is the other open question. Stanford's Jared Duker Lichtman noted that getting the whole thing into Mathlib "would be quite an achievement"; Axiom says upstreaming "as much of it as is reasonable" is the long-term goal.