Axiom Math releases Lean formalization of the Stacks Project algebraic geometry textbook

Axiom Math says it has released a 16-million-line Lean formalization of the Stacks Project, a reference textbook on algebraic geometry.

Lean checks each completed proof, and each tagged result links to its original text and dependencies, according to the announcement on X by Rohan Paul.

Axiom Math describes the library as free and open source, so that mathematicians and AI models can reuse its verified definitions and theorems. The company says the code keeps the textbook's highly interconnected structure and has been optimized for code quality.