Axiom has released an open-source Lean formalization of the Stacks Project, the collaborative algebraic geometry reference Johan de Jong began at Columbia in 2005, now roughly 7,500 pages. The library covers every Stacks tag with formalizable content in about 16 million lines of Lean, built on Mathlib. The project site lists 62,975 files, 663,090 declarations, and 15.8 million lines. Each declaration keeps the original four-character tag, so the Stacks text can be read beside the Lean code, with the dependency graph at stacks.axiommath.ai. The library is for algebraic geometers, Lean developers, and AI systems that need checked definitions and theorems they can import into new proofs. A current argument in the field often rests on a long chain through commutative algebra, schemes, sheaves, cohomology, and algebraic stacks, and that chain had no Lean library covering the full reference. Axiom, the AI math company Carina Hong founded in 2025, used coordinated agents to translate statements, search Mathlib for existing abstractions, and keep definitions aligned across chapters. Lean's kernel checks every completed proof. People have reviewed StacksCore against the Stacks text and brought it toward Mathlib style. StacksFrontier was written by agents and still needs that review before it moves into StacksCore. Proofs use only Lean's standard axioms, with no sorry and no native_decide. The agents found dozens of statements that needed local repair, including missing hypotheses and claims that failed in the generality written, and they recorded counterexamples with corrected versions. Where a supporting lemma failed, they looked for another route to the main result. The code is Apache 2.0 and is maintained apart from the upstream Stacks Project, which stays with de Jong and its contributors. Exercises, examples, and remarks remain open, and the project asks mathematicians and Lean developers to review agent-written code and formalize what is left.