Axiom Math releases a Lean formalisation of the Stacks Project

Axiom Math released a Lean formalisation of the Stacks Project, the open-source reference on the foundations of algebraic geometry that Columbia University mathematician Johan de Jong began in 2005. Axiom describes it as spanning some 16 million lines of code and as “the largest integrated, reusable library of formalized mathematics ever built”. The superlative is the company’s own claim, and the account here rests on Axiom’s post. The release came days after Axiom’s formalisation of the classification of finite simple groups.

Lean is a proof assistant whose kernel checks every step mechanically. Axiom says the Stacks work differs from the earlier release because the Stacks Project is a library of interlocking definitions and lemmas meant for reuse, rather than a route to a single landmark theorem. The library keeps the project’s permanent four-character tags, and a companion site shows the original text beside the Lean code and a dependency graph.

Axiom says it built the library with a hierarchical system of AI agents that translated statements, searched Mathlib (the community Lean library) for existing definitions, built proofs and resolved prerequisites in parallel. The company acknowledges the central risk of such a process: a Lean proof can be correct while the formal statement fails to capture the mathematics, and it says ensuring faithfulness is “even more important than verifying its proof”. Its answer is automated: multi-agent auditing and cross-checks against the source text, plus targeted audits of foundational definitions and landmark theorems. The post does not describe a line-by-line human review of the full library.

Axiom also reports that the process turned up “dozens” of statements in the Stacks Project that needed local refinement, including missing hypotheses, edge cases in positive characteristic and claims that did not hold in the generality stated, and that its agents built explicit counterexamples. These findings are Axiom’s, and the post does not list them for outside checking.

The post says de Jong, in an announcement of 21 October 2026, asked that AI-generated comments and pull requests not be submitted directly to the upstream Stacks repository for the time being. Axiom states that its formalisation is an independent project it maintains itself, and that it is keeping its counterexamples and refinements in its own repository, where mathematicians can review them.

The release extends a cluster of Lean-checked results from AI developers, including the exponential time hypothesis claims of late October, where review by human experts was still pending.