Axiom released a 16 million line open-source Lean formalization of the entire Stacks Project, a foundational algebraic geometry reference work. Built by an AI agent swarm, all proofs are machine-checked by Lean’s kernel, preserving the original’s interconnected structure of thousands of definitions, lemmas and theorems. The library is available at stacks.axiommath.ai with contribution guidelines for further formalization and review.
Axiom’s Stacks Project Lean formalization provides a connected library of algebraic-geometry definitions and results, built on Mathlib and organized around the original text’s permanent tags. Its website lets readers search the library, inspect Lean declarations alongside Stacks references, and explore an interactive dependency graph. The repository distinguishes human-reviewed StacksCore code from AI-agent-written StacksFrontier code; Lean’s kernel checks proofs in both. Contributors can formalize remaining examples and exercises, review code, and improve existing proofs.
Mathlib is the mathematical library on which the Stacks formalization is built.
