The Stacks Project, formalized in Lean | Axiom

Axiom has released a Lean formalization of the entire Stacks Project, creating a 16-million-line machine-checked library for modern algebraic geometry. By deploying coordinated AI agent swarms, the company translated and integrated thousands of theorems while preserving the original reference's permanent tag structure. The open-source library aims to provide researchers and AI agents with a verified, reusable foundation for future mathematical proofs. Open article →