The Stacks Project, Formalized in Lean

Axiom has released a complete Lean formalization of the Stacks Project, a 7,500-page foundational reference in algebraic geometry, comprising 16 million lines of machine-checked code—the largest integrated formalized mathematics library ever built. The formalization enables researchers and AI systems to directly import and use the Stacks Project's definitions and theorems in new proofs, addressing the growing need for formal verification as AI generates mathematical arguments at unprecedented speeds. This achievement required coordinated AI agents to translate thousands of theorems in parallel and represents a major step forward in formalizing modern algebraic geometry and its dependent fields.