Axiom Formalizes Stacks Project in Lean Using AI Agents
The result argues that at-scale AI code generation can meet formal verification standards, not just quick prototypes. Mathematics researchers and formal-methods teams gain a machine-checked base they can build on, and it signals AI agents moving from toy proofs to large structured libraries. It also compares favourably with prior partial formalization efforts in scope and coherence.
Axiom has formalized the Stacks Project in Lean, converting a large foundation of algebraic geometry into machine-checkable mathematics. The formalization covers a deeply interconnected structure where every definition and proof links across chapters. A human-led swarm of AI agents built the corpus, which can now serve as a reusable base for AI agents doing mathematics. Axiom presents the release as a counterexample to claims that AI-generated code is inherently sloppy.
AI-generated code at scale usually gets written off as sloppy. Axiom's new release is a strong counterexample.
Axiom says it has formalized the Stacks Project in Lean, a huge, deeply interconnected foundation of algebraic geometry, turning it into mathematics a computer can check.
The impressive part isn't just the size, it's the structure. Axiom compares it to the Louvre's glass pyramid: individual pieces that only work because they fit together into something much bigger. Every definition and proof has to connect, so a result proved in one chapter can be used in another.
That's what makes it more than a translation. A human-led swarm of AI agents built a reusable, machine-checkable foundation that AI agents can now use to do mathematics.
Congrats to the Axiom team!
