Axiom, the AI math company, has released a Lean version of every part of the Stacks Project, the open-source reference that holds up modern algebraic geometry. The company announced it on its research blog on 4 November 2026. Axiom says the result runs to roughly 16 million lines of code and is the biggest reusable, connected body of machine-checked math anyone has assembled. That superlative is the company’s own, and the post offers no outside comparison.
Lean is a proof assistant: a program whose kernel refuses any argument that does not follow from its stated assumptions. A library written in it can be imported like software, so a new proof can cite an old theorem and the machine confirms the citation is legitimate. Axiom’s pitch is that algebraic geometry never had such a foundation. A single modern proof can lean on a long chain of results about rings, schemes, sheaves, and cohomology before its own argument starts, and that chain existed only on paper.
The paper version is the Stacks Project, which Columbia mathematician Johan de Jong started in 2005. It now spans about 7,500 pages and thousands of four-character tags. Every theorem carries a proof, and every step points to the tags it depends on. Axiom’s reading is that de Jong built something close to a dependency graph long before anyone formalized it, which is why the translation was feasible at all. The formalization also rests on years of work by the Lean and Mathlib communities (Mathlib is the shared open-source math library for Lean).
The harder part was keeping the pieces consistent. Axiom describes a hierarchy of AI agents that translated statements, searched Mathlib for existing definitions, wrote proofs, and settled prerequisites in parallel. Without coordination, the company says, two agents will each prove sound theorems on one shared object using slightly different definitions, and Lean will accept both files while making them hard to combine. Axiom also audits that each Lean statement says what the original text says, since a proof of a watered-down claim proves nothing useful.
Axiom also says the original text had holes. It reports that its system surfaced dozens of Stacks statements that needed repair, among them absent assumptions, odd cases in positive characteristic, plus claims that broke when applied as broadly as written. In those cases the agents built explicit counterexamples, formalized corrected versions, and in some cases found other routes through the literature so that deeper theorems still held under their original assumptions. The post gives no list of the affected statements.
Those fixes will not flow upstream any time soon. In an announcement dated 21 October 2026, he asked that comments and code changes written by AI stay out of the upstream repository for now. Axiom says it respects that and keeps its counterexamples and refinements in its own repository, with a viewer at stacks.axiommath.ai that sets the original pages beside the Lean code.
The release arrives eight days after Axiom published its Lean version of the finite simple groups classification (CFSG). The two projects differ in kind. The classification is built around one landmark theorem, while the Stacks Project is a toolbox meant to be reused. That makes it the more useful test of whether AI-written formal libraries can serve as shared infrastructure rather than one-off trophies.
Anyone planning to cite the counterexamples should check them against the printed Stacks text first, because the only review so far is Axiom’s own.
Reported by Axiom Math on its research blog, 4 November 2026.
