Axiom puts the 7,500-page Stacks Project into Lean, turning algebraic geometry's foundations into an importable machine-checked library
Synopsis
Axiom released a Lean formalization of the Stacks Project, turning the roughly 7,500-page open reference that lays the foundations of modern algebraic geometry into a single machine-checked library of about 16 million lines of code. Algebraic geometry had lacked matching Lean infrastructure: a contemporary proof may invoke a long chain of theorems across commutative algebra, schemes, sheaves, cohomology and algebraic stacks before its core argument begins. The library keeps the original permanent tags so researchers and AI agents can import definitions and theorems directly, and the formalization surfaced dozens of statements needing local refinement.
Interpretation
The foundational literature of modern algebraic geometry now has a formalized, machine-checked Lean library that researchers and AI agents can import into new formal proofs. Algebraic geometry had been hard to approach this way: a contemporary proof may invoke a long chain of theorems across commutative algebra, schemes, sheaves, cohomology and algebraic stacks before its core argument begins, and the mathematics existed in the Stacks Project while the corresponding Lean infrastructure did not. The release covers the full mathematical development of the Stacks Project at roughly 16 million lines of code, which the releasing organization describes as the largest integrated, reusable library of formalized mathematics ever built.
The library preserves the original permanent four-character tags, so every Lean declaration links back to the canonical text mathematicians already know, and readers can view original pages side by side with the corresponding Lean code. A single Stacks tag often unfolds into multiple formal definitions and lemmas, some newly defined and others bridged directly to existing Mathlib declarations, and the interface tracks these mappings explicitly. The site stacks.axiommath.ai offers side-by-side text and Lean code plus an interactive dependency graph, while the formalization is an independent open-source project maintained by Axiom.
Formalization also checked the source: the system surfaced dozens of statements in the Stacks Project that required local refinement, including missing hypotheses, edge cases in positive characteristic, and claims that did not hold in the full generality stated. Failed proof attempts were not treated as mere obstacles; agents diagnosed the underlying mathematical obstructions and constructed explicit counterexamples to show where the original statements broke down. For local oversights, agents identified the exact missing hypotheses and formalized corrected theorems alongside their counterexamples; where a false supporting lemma created a gap in a deeper theorem, agents found alternative routes through the literature to establish the main result under its original hypotheses.
Perspective
The demonstrated scope is a Lean formalization of the full mathematical development of the Stacks Project, together with a companion interface for side-by-side text and formal code, dependency-graph tracing and counterexample inspection; the formalization is an independent open-source project maintained by Axiom, separate from the upstream Stacks Project repository.
The source states that on October 21, 2026, de Jong requested that AI-generated comments and pull requests not be submitted directly to the upstream Stacks Project repository for the time being; source corrections are given as a count of dozens of statements without a per-item list, and whether upstream has adopted them is not stated.