Axiom Math releases a Lean formalisation of the Stacks Project
About 16 million lines of Lean cover the roughly 7,500-page algebraic-geometry reference; Axiom says its agents found dozens of statements in the original needing correction.
Axiom MathIdeas & essays