Axiom says it has formalised the whole Stacks Project in Lean
Axiom released a Lean formalisation of the Stacks Project, the open reference for the foundations of algebraic geometry, built by coordinated AI agents. The Lean kernel checks every proof, but the agent-written part has not yet been reviewed by people and checking proofs does not show that statements match the source.
Source published · In the Weekly Review of 8 November 2026
Filed under Mathematics
The Stacks Project, started by Johan de Jong in 2005, runs to about 7,500 pages. Axiom said on 4 November that every tag with formalisable content now has a Lean counterpart without gaps, linked to the canonical Stacks tags, and that the work rests on Lean and Mathlib.
The company’s argument is that modern proofs in the field depend on long chains of results in commutative algebra, schemes, cohomology and stacks that had no Lean foundations. The claims have not yet been evaluated independently.