Axiom Formalizes the Entire Stacks Project in Lean: a Roughly 7,500-Page Algebraic Geometry Reference Becomes About 16 Million Lines of Machine-Checked Code, and Agents Flag Dozens of Statements Needing Fixes

A reference book you can now import

Math AI company Axiom released a Lean 4 formalization of the Stacks Project on November 4, with the code under Apache 2.0 in the AxiomMath/Stacks repository on GitHub. The Stacks Project, started in 2005 by Columbia University mathematician Johan de Jong, is an open-source algebraic geometry reference of about 7,500 pages in which every result has a permanent four-character tag. Axiom says the formalization runs to about 16 million lines of code, is built on Lean v4.34.0-rc2 and Mathlib, and covers every tag with formalizable content; examples, exercises and remarks are not finished and are listed as tasks for contributors. The README states there is no sorry and that proofs rest only on Lean's three standard axioms; the library has about 63,000 modules, so a full build is slow and memory-hungry.

The practical gain: someone formalizing a new theorem about families of curves no longer has to rebuild schemes or cohomology from scratch and can cite existing definitions and theorems instead. Each Lean declaration points back to its book entry with @[stacks TAG], and stacks.axiommath.ai shows the original text side by side with the Lean code.

AI-written and human-reviewed code kept apart

Axiom used a hierarchy of coordinated agents to translate statements, search Mathlib for existing abstractions, build proofs and keep interfaces consistent across chapters. The repository splits the code into two tiers: StacksCore has been checked by people against the book and brought to Mathlib standards, while StacksFrontier was written by agents and still awaits human review. Lean's kernel checks proofs in both, but whether each formal statement faithfully matches the text is enforced mainly through multi-agent auditing and semantic cross-checks, with human audits limited to foundational definitions and landmark theorems.

Problems found in the source text

Axiom says the work surfaced dozens of original statements needing local refinement: missing hypotheses, edge cases in positive characteristic and claims that do not hold in the stated generality. The agents built counterexamples for these, and where a false supporting lemma undercut a deeper theorem they found alternative proofs in the literature. De Jong asked on October 21 that AI-generated comments and pull requests not be sent upstream for now, and Axiom says its corrections and counterexamples stay in its own repository for mathematicians to use on their own terms. The corrections are so far disclosed only by Axiom and have not been confirmed item by item by the Stacks Project maintainers.