Axiom releases Lean formalization of the entire Stacks Project

Axiom has released a Lean formalization of the entire Stacks Project, the roughly 7,500-page open-source reference that lays the foundations of modern algebraic geometry. Axiom says the result spans some 16 million lines of code and is the largest integrated, reusable library of formalized mathematics ever built. The full development is available as a single, machine-checked library. Researchers and AI agents can import its definitions and theorems into new formal proofs, and permanent Stacks tags link every Lean declaration back to the original text.

The Stacks Project was initiated by Columbia University mathematician Johan de Jong in 2005. It grew from an introduction to algebraic stacks into a living, collaborative encyclopedia with thousands of permanent four-character tags, written by hundreds of contributors over two decades. Its editorial rules are strict: every theorem carries a proof, every assumption is stated explicitly, and every step points back to the exact tags it depends on. Axiom argues that this design anticipated the architecture of formal proof libraries, with stable identifiers and explicit dependency graphs. Axiom also credits the Lean and Mathlib communities, saying a corpus of this size was only possible because they spent years building a rich mathematical library.

Axiom's case for doing it: as AI systems generate mathematical arguments faster than humans can check them, formal verification becomes essential. In fields with mature Lean infrastructure, new results can often be formalized soon after discovery. Modern algebraic geometry was far harder to approach this way, because a single contemporary proof may invoke a long chain of results across commutative algebra, schemes, sheaves, cohomology and algebraic stacks. The mathematics existed in the Stacks Project, but the Lean infrastructure did not.

Axiom frames the job as software engineering as much as mathematics. Uncoordinated AI code generation can produce short, isolated scripts quickly, but millions of lines of verified mathematics need clean abstractions and stable interfaces. If thousands of agents formalize theorems in parallel without coordination, two agents can prove correct theorems about the same object using subtly incompatible definitions, or duplicate infrastructure already in Mathlib; Lean's kernel would accept both files, yet the results would be hard to compose. So Axiom's mathematicians and engineers designed a hierarchical system of AI agents with specialized responsibilities and strict coordination protocols. Agents worked in parallel across the dependency graph to translate statements, search Mathlib for existing abstractions, construct proofs and resolve prerequisites, keeping definitions, typeclass interfaces and abstractions aligned across chapters.

Axiom says that checking faithfulness of each formal statement matters even more than checking its proof. It enforces faithfulness through multi-agent auditing, semantic cross-checks against the source text, and the requirement that every definition and lemma interface with the downstream theorems that depend on it, combined with targeted audits of foundational definitions and landmark theorems.

The process also exposed problems in the original text. Axiom says its system surfaced dozens of Stacks Project statements that needed local refinement: missing hypotheses, edge cases in positive characteristic, and claims that did not hold in the full generality stated. The agents built explicit counterexamples to show where the original statements broke down, identified the exact missing hypotheses, and formalized corrected theorems alongside the counterexamples. Where a false supporting lemma left a gap in the proof of a deeper theorem, the agents found alternative routes through the literature to establish the main result under its original hypotheses.

For navigation, the release keeps the original tag structure. At stacks.axiommath.ai, readers can view Stacks Project pages side by side with the corresponding Lean code and explore an interactive dependency graph. Because one Stacks tag often unfolds into several formal definitions and lemmas, some new and some bridged to existing Mathlib declarations, the interface tracks those mappings explicitly.

Axiom notes that on October 27, 2026 it released a Lean formalization of the Classification of Finite Simple Groups (CFSG). It contrasts the two: CFSG is organized around a single landmark theorem, while the Stacks Project is a foundational library of interlocking definitions, constructions and lemmas meant for reuse.

On governance, Axiom reports that in an October 21, 2026 announcement de Jong requested that AI-generated comments and pull requests not be submitted directly to the upstream Stacks Project repository for the time being. The Stacks Project remains a living text under de Jong's stewardship, while the Lean formalization is an independent open-source project maintained by Axiom. Axiom says it respects that boundary and keeps its formalization, counterexamples and refinements in its own repository, where mathematicians can review them on their own terms.

Key facts

Axiom released a Lean formalization of the whole Stacks Project, the roughly 7,500-page algebraic geometry reference, spanning some 16 million lines of code.
Axiom says coordinated swarms of AI agents, organized as a hierarchical system with strict coordination protocols, translated, proved and integrated thousands of theorems in parallel.
The system surfaced dozens of Stacks statements needing local refinement, such as missing hypotheses and edge cases in positive characteristic, and built explicit counterexamples for some.
Permanent Stacks tags link each Lean declaration to the original text; stacks.axiommath.ai shows pages side by side with the Lean code and an interactive dependency graph.
Johan de Jong asked on October 21, 2026 that AI-generated comments and pull requests not go to the upstream Stacks repository for now, so Axiom keeps its work in its own repository.

Why it matters

Axiom argues that AI systems are starting to produce mathematical arguments faster than people can inspect them, which makes formal verification essential. Modern algebraic geometry has been hard to formalize because even one contemporary proof can rest on a long chain of results from commutative algebra to algebraic stacks. A machine-checked library of the Stacks Project, the field's foundational reference, is meant to remove that barrier. Axiom calls it the largest integrated, reusable library of formalized mathematics ever built; that is the company's own claim. The release also shows a side effect it highlights: formalization found statements in the human-written text that were not true as stated.

Who it affects

Researchers in algebraic geometry and neighbouring fields that rely on its machinery, who can import definitions and theorems instead of rebuilding foundations such as schemes or coherent cohomology. AI agents that attempt formal proofs get the same library. The Stacks Project community and Johan de Jong are affected as well, since the formalization found statements that needed refinement, and de Jong has asked that AI-generated contributions stay out of the upstream repository for now. The Lean and Mathlib communities are the base the work builds on, and some of the new Lean declarations are bridged to existing Mathlib ones.

How to use it

At stacks.axiommath.ai you can read the original Stacks Project pages next to the matching Lean code and browse the interactive dependency graph. A mathematician or an AI agent formalizing a new result, for example about families of curves, can import the relevant definitions and theorems directly, and Lean's kernel applies each cited result only when its exact hypotheses are met. Permanent Stacks tags map every Lean declaration back to the canonical text. Corrections and counterexamples live in Axiom's own repository, not in the upstream Stacks Project, which asks for no AI-generated comments or pull requests for the time being.

How solid is it

The source is Axiom's own release post, so the size, the scale and the superlative are the company's claims. The post gives the figures as approximate: roughly 7,500 pages and some 16 million lines. It describes its faithfulness checks (multi-agent auditing, semantic cross-checks against the source text, downstream interface requirements, targeted audits of foundational definitions and landmark theorems) but reports no independent verification or outside reaction. The number of refined statements is given only as dozens, and the post does not list them. It does not give the number of agents, the compute cost, the timescale or the models used.

Risks and caveats

Axiom itself stresses that a formal statement can be accepted by Lean's kernel yet fail to capture the meaning of the original text, which is why it treats faithfulness as more important than proof checking; its faithfulness pipeline is largely automated, with targeted audits on foundational definitions and landmark theorems. Uncoordinated parallel work can also yield incompatible definitions that are hard to compose. There is a community boundary too: de Jong asked that AI-generated comments and pull requests not be submitted upstream, so the corrections Axiom found live in a separate repository that mathematicians can review on their own terms. The Lean formalization is maintained by Axiom as an independent project, while the Stacks Project itself stays a living text under de Jong's stewardship.

“Spanning some 16 million lines of code, it is the largest integrated, reusable library of formalized mathematics ever built.”

— Axiom, release post