The Stacks Project, formalized in Lean

Axiom has released a complete Lean formalization of the Stacks Project, the roughly 7,500-page open-source algebraic geometry reference initiated by Columbia University mathematician Johan de Jong in 2005. The formalization spans about 16 million lines of code, making it the largest integrated, reusable library of formalized mathematics ever built, with permanent Stacks tags linking each Lean declaration to the canonical text. Axiom said the effort relied on years of prior work by the Lean and Mathlib communities and used coordinated swarms of AI agents to translate, prove and integrate thousands of theorems in parallel. The release matters because formal verification is becoming essential as AI systems generate mathematical arguments faster than humans can inspect them, and algebraic geometry had lacked the Lean infrastructure to keep pace. Researchers and AI agents can now import the library's definitions and theorems directly into new formal proofs. Next to watch is whether the formalization accelerates machine-checked work in algebraic geometry and neighboring fields that depend on its machinery.