Axiom formalizes the entire Stacks Project in Lean, creating the largest machine-checked math library ever built
The Stacks Project, Formalized in Lean
Axiom has released a Lean formalization of the Stacks Project, the 7,500-page open-source foundation of algebraic geometry, spanning 16 million lines of code. Coordinated swarms of AI agents translated and proved thousands of theorems in parallel, preserving the project's permanent tags and linking every Lean declaration back to the original text. The library is open source and available at stacks.axiommath.ai, where researchers can view the formal code side-by-side with the canonical source and explore the dependency graph.
Rather than treating failed proof attempts as mere obstacles, our agents diagnosed the underlying mathematical obstructions and constructed explicit counterexamples to prove where the original statements broke down.