The Stacks Project, Formalized in Lean

Axiom announces a Lean formalization of the Stacks Project, a roughly 7,500-page collaborative reference for modern algebraic geometry. The release comprises about 16 million lines of code, assembled into one machine-checked library whose definitions and theorems can be reused in future proofs. Permanent tags connect Lean declarations to the corresponding parts of the original text, and an online interface displays the text alongside code and interactive dependency graphs. The project addresses a major barrier to formalizing contemporary mathematics: algebraic geometry relies on long chains of results across areas such as commutative algebra, schemes, sheaves, and cohomology. A unified library lets researchers and AI systems build on verified foundations rather than reconstruct them.

The work’s central challenge was not simply proving thousands of isolated results, but ensuring their definitions and interfaces fit together coherently. Axiom says coordinated AI agents worked across the dependency graph to translate statements, reuse Mathlib abstractions, prove results, and audit their fidelity to the source. Lean’s kernel checks proofs, while cross-checks and downstream dependencies help detect statements that misrepresent the mathematics. Formalization also exposed dozens of claims needing refinement, including missing hypotheses, positive-characteristic edge cases, and statements false in their stated generality. Agents produced counterexamples, corrected local results, and found alternate proofs where needed. The release presents formal verification both as infrastructure for future algebraic geometry and as a method for finding and repairing weaknesses in mathematical literature.