The Stacks Project, formalized in Lean
Axiom says it has released a Lean formalization of the entire Stacks Project, the extensive algebraic-geometry reference, as a connected library of roughly 16 million lines. It says coordinated AI agents translated and proved material against shared interfaces, with original Stacks tags mapping the formal declarations back to the text.
The claim of complete, faithful coverage deserves independent scrutiny: kernel-checked proofs establish their formal statements, not automatically that those statements capture the intended mathematics. HN readers highlighted the value of a reusable foundation and asked how the translation of hypotheses was checked; others worried about human understanding of generated mathematics.