Axiom publishes a Lean formalisation of the Stacks Project
The library covers every Stacks tag with formalisable content, and Lean’s kernel checks each proof. Much of it is AI-written code that has not yet had human review.
In the Daily Brief of 5 November 2026
Filed under Mathematics
The Stacks Project is the open-source reference work on algebraic geometry. Axiom’s library builds on Mathlib and has two tiers. StacksCore has been checked by people against the source and brought to Mathlib standards. StacksFrontier was written by AI agents and still awaits that review.
The repository says there is no sorry and no native_decide, and declarations also carry references to the items of Grothendieck’s EGA and SGA that they prove. Examples, exercises and remarks are left to contributors. Kernel checking confirms that a proof is valid, and it does not show that a formal statement says what the source says.