Axiom releases a Lean formalization of the entire Stacks Project, about 16 million lines built by AI agent swarms
The roughly 7,500-page algebraic geometry reference is now one machine-checked library; outside mathematicians have not yet reviewed how faithful the statements are.
Why it matters
Modern algebraic geometry has had little Lean infrastructure, because a single proof can depend on long chains of results in commutative algebra, schemes, sheaves and cohomology. Axiom says its library keeps the Stacks Project's permanent tags, so people and AI agents can import its definitions and theorems directly into new proofs. It follows Axiom's Lean formalization of the Classification of Finite Simple Groups on October 27, 2026. The thing to watch is whether mathematicians who check the statements against the original text find them faithful, and whether the library is taken up alongside Mathlib.
Key facts
- Stacks Project: roughly 7,500 pages
- About 16 million lines of Lean code
- Built with coordinated swarms of AI agents
- Started by Johan de Jong of Columbia University in 2005
- Viewable at stacks.axiommath.ai
- Follows Axiom's CFSG formalization of October 27, 2026