Today, Axiom is releasing our Lean formalization of the entire Stacks Project, the roughly 7,500-page open-source reference that lays the foundations of modern algebraic geometry. Spanning some 16 million lines of code, it is the largest integrated, reusable library of formalized mathematics ever built.
With this release, the full mathematical development of the Stacks Project is available as a single, machine-checked library. Researchers and AI agents alike can import its definitions and theorems directly into new formal proofs, while permanent Stacks tags link every Lean declaration back to the canonical text mathematicians already know.
This milestone begins with the Stacks Project itself. Initiated by Columbia University mathematician Johan de Jong in 2005, it has grown through the tireless work of hundreds of mathematicians who have contributed proofs, examples, and refinements over two decades. Our formalization rests equally on the foundations of the Lean and Mathlib communities. Formalizing a corpus of this magnitude was only possible because those communities spent years building a rich mathematical library, along with the abstractions needed to organize it, long before our work began.
