The Stacks Project, formalized in Lean

Published 6 November 2026

Axiom has formalized the entire Stacks Project as a single machine-checked Lean library, allowing researchers and AI agents to reuse its algebraic geometry proofs in new formal developments.