The Stacks Project, formalized in Lean
Summary
Axiom releases a Lean formalization of the Stacks Project, a 7,500-page open-source reference for modern algebraic geometry, backed by a massive codebase. The article explains that researchers and AI agents can import definitions and theorems directly and view side-by-side with the original text, supported by explicit dependency graphs. It also discusses the engineering challenges of coordinating thousands of AI agents to maintain a coherent, reusable formal library and the future impact on mathematical research.