Axiom Math formally verifies the Stacks Project: 7,654 pages of algebraic geometry become 16 million lines of checked Lean

On Wednesday, Axiom Math said its AI agents had finished one of the largest checking jobs in mathematics: a complete formal verification of the Stacks Project, the open reference that underpins modern algebraic geometry. The result is roughly 16 million lines of Lean code — a machine-checked library Axiom describes as the largest integrated collection of formalized mathematics ever built.

The Stacks Project is not a single theorem. Begun in 2005 by Columbia mathematician Johan de Jong, it is an open reference spanning undergraduate algebra to the frontiers of algebraic geometry and number theory — about 7,654 pages, assembled over two decades by hundreds of contributors. Turning it into Lean meant translating every definition and proof into code a proof assistant can check step by step, while keeping the whole web of dependencies intact.

Why algebraic geometry was the hard case#

Formal verification is straightforward to describe and hard to scale. A proof written in Lean is checked line by line by the Lean kernel: if it compiles, every step follows from the axioms. The difficulty with the Stacks Project is not any single proof but the connections between thousands of them — a theorem deep in the text can depend on a long chain of earlier results.

That density is why the field had a gap: researchers who wanted to verify new work in algebraic geometry had little to build on, because the foundations did not exist in machine-checked form. Closing it means a mathematician — or an AI agent — proving a new result can now import the foundations instead of rebuilding them.

The timing matters beyond mathematics. AI systems are now producing mathematical arguments faster than humans can read them, and the automated checks meant to confirm such results can themselves fail. A verified library gives those systems something to build on that has actually been checked, rather than something that merely sounds right.

How the agents built it#

Axiom did not hand the job to a single model. Its engineers built a hierarchical system of AI agents with defined responsibilities and strict coordination rules, then set them loose across the dependency graph in parallel: some translated statements, some searched Mathlib for existing abstractions to reuse, some constructed proofs, and others resolved prerequisites — all while keeping definitions and interfaces aligned across chapters.

The coordination is the point. Thousands of agents formalizing theorems independently would produce correct proofs about subtly incompatible definitions — results the Lean kernel accepts in isolation but cannot be combined. Axiom also trained its own models for mathematical reasoning rather than relying only on general-purpose systems, and started with an in-house Lean expert teaching the agents judgment about which formalizations were worth writing.

The formalization fought back#

The process did more than transcribe. Axiom says its system surfaced dozens of statements in the Stacks Project that needed local fixes — missing hypotheses, edge cases in positive characteristic, and claims that did not hold in the full generality stated. Where a proof attempt failed, the agents diagnosed the obstruction, built explicit counterexamples showing where the statement broke down, and repaired the mathematics so later chapters could still depend on it.

That is the part mathematicians will read most closely. A formalization that only ever confirms the source text is less interesting than one that finds where the text was wrong — and Axiom is publishing the counterexamples and corrections in its own repository alongside the library.

What it is — and what it isn’t#

Two caveats belong in any honest account. First, a Lean check confirms that each proof follows from its axioms; it does not by itself confirm that the formal statement captures the theorem a reader of the original text had in mind. Axiom says it guards against that with multi-agent auditing, semantic cross-checks against the source, and targeted audits of foundational definitions and landmark theorems — but no independent audit of the translation has been published yet.

Second, the formalization is Axiom’s own project, not the Stacks Project’s. On October 21, de Jong asked that AI-generated comments and pull requests not be submitted directly to the upstream repository for now. Axiom says it respects that boundary, keeping its formalization, counterexamples, and refinements in its own repository, where the Stacks Project community can review them on its own terms. The release preserves the project’s permanent tag system, so every Lean declaration links back to the canonical text, and a side-by-side viewer at stacks.axiommath.ai lets readers compare the original pages with the code.

Why it matters#

For working mathematicians, the immediate value is practical: the foundations of algebraic geometry are now importable. For AI research, the value is structural. If agents are going to do mathematics, they need verified ground to stand on, not a pile of plausible-looking text. A 16-million-line checked library is the largest such ground anyone has built.

What to watch: whether independent mathematicians audit the translation and find the formal statements faithful; whether new results in algebraic geometry start being formalized against the library soon after they appear; and whether Axiom’s challenge to other AI companies — to attempt formalization at this scale — gets taken up. The company, founded in March 2025 by former Stanford math PhD student Carina Hong, raised a $200 million Series A led by Menlo Ventures and is valued at $1.6 billion, according to TechCrunch — a bet that verified mathematics becomes infrastructure, not a curiosity.

Sources: Axiom Math, ‘The Stacks Project, formalized in Lean’ (November 5, 2026), here; TechCrunch, ‘Axiom Math wants to keep AI slop out of mathematics’ (November 5, 2026), here.