Axiom says it has formalised the entire Stacks Project in Lean
The company says the roughly 7,500-page reference on algebraic geometry is now a single machine-checked library of about 16 million lines. The claim has not been independently reviewed.
Source published · In the Daily Brief of 6 November 2026
Filed under Mathematics
The Stacks Project, started by Johan de Jong of Columbia University in 2005, is the open-source reference for the foundations of modern algebraic geometry, built by hundreds of mathematicians. Axiom said on 4 November that it had released a Lean formalisation of the whole text, with each declaration linked to the canonical Stacks tags, and described it as the largest integrated reusable library of formalised mathematics.
The company says the work rests on Lean and Mathlib and was done by coordinated swarms of AI agents translating, proving and integrating theorems in parallel. Its case for the project is that a contemporary proof in the field can depend on a long chain of results in commutative algebra, schemes, cohomology and stacks, which until now lacked Lean foundations.