Axiom releases Lean formalization library of the Stacks Project

Axiom has released a complete Lean formalization of the Stacks Project, covering approximately 7,500 pages of foundational literature on algebraic geometry, with a codebase of about 16 million lines, which it calls the largest reusable formalized mathematics library to date. The library preserves the original text's permanent Stacks tags, and every Lean declaration can be traced back to the corresponding original text, allowing researchers and AI agents to directly import definitions and theorems. Axiom stated that the translation and proofs were completed through layered multi-agent collaboration, and that during the process dozens of statements in the original text were found to require additional hypotheses or corrections.