THE STACKS PROJECT, FORMALIZED IN LEAN

Summary from the TLDR AI newsletter

Axiom has released a Lean formalization of the entire Stacks Project. The Stacks project is an open-source reference that lays the foundation of modern algebraic geometry. The release is the largest integrated, reusable library of formalized mathematics ever built. It makes the full mathematical development of the Stacks Project available as a single, machine-checked library that researchers and AI agents can import from directly into new formal proofs.