The Stacks Project, formalized in Lean

Today, Axiom is releasing our Lean formalization of the entire Stacks Project, the roughly 7,500-page open-source reference that lays the foundations of modern algebraic geometry. Spanning some 16 million lines of code, it is the largest integrated, reusable library of formalized mathematics ever built.

With this release, the full mathematical development of the Stacks Project is available as a single, machine-checked library. Researchers and AI agents alike can import its definitions and theorems directly into new formal proofs, while permanent Stacks tags link every Lean declaration back to the canonical text mathematicians already know.

This milestone begins with the Stacks Project itself. Initiated by Columbia University mathematician Johan de Jong in 2005, it has grown through the tireless work of hundreds of mathematicians who have contributed proofs, examples, and refinements over two decades. Our formalization rests equally on the foundations of the Lean and Mathlib communities. Formalizing a corpus of this magnitude was only possible because those communities spent years building a rich mathematical library, along with the abstractions needed to organize it, long before our work began.

Why formalize a foundational reference of this scale? As AI systems begin generating mathematical arguments at a pace far beyond what humans can inspect by hand, formal verification becomes essential. In fields with mature Lean infrastructure, new results can often be formalized shortly after they are discovered. Until now, modern algebraic geometry has been far harder to approach this way: a single contemporary proof may invoke a long chain of theorems across commutative algebra, schemes, sheaves, cohomology, and algebraic stacks before its core argument even begins. The mathematics existed in the Stacks Project, but the corresponding Lean infrastructure did not.

Closing that gap is as much a software engineering challenge as a mathematical one. While uncoordinated AI code generation can produce short, isolated scripts quickly, scaling to millions of lines of verified mathematics requires clean abstractions, stable interfaces, and components that fit together across an entire codebase. To achieve this, we deployed coordinated swarms of AI agents capable of translating, proving, and integrating thousands of theorems in parallel. Formalizing the Stacks Project in its entirety establishes a new starting point for algebraic geometry and the many neighboring fields that rely on its machinery.

At its heart, algebraic geometry studies the interplay between algebraic equations and the geometric shapes they describe. Over the real numbers, the equation $x^2 + y^2 = 1$ defines a circle; over the rational numbers, its points correspond to Pythagorean triples, such as $3^2 + 4^2 = 5^2$. Studying the same equations across different number systems, or in families that vary over a parameter space, connects geometry directly to number theory and algebra. These ideas also reach beyond pure mathematics: elliptic curves secure modern digital cryptography, while algebraic curves over finite fields power error-correcting codes. Modern algebraic geometry provides a common language for studying equations across all of these settings.

Forging that language took generations. Emmy Noether revolutionized algebra by shifting focus from individual equations to abstract structures such as rings, modules, and ideals. Just as the right software abstraction can replace thousands of special-purpose routines with a single reusable framework, a theorem proved for the right algebraic structure applies across many concrete settings at once. A generation later, Alexander Grothendieck and his collaborators introduced the theory of schemes, creating a sweeping dictionary between algebra and geometry that allowed mathematicians to do geometry over arbitrary rings, with arithmetic and infinitesimal data built in from the start. Monumental treatises like Éléments de géométrie algébrique (EGA) and Séminaire de géométrie algébrique du Bois Marie (SGA) rebuilt the foundations of the discipline from the ground up, supplying the machinery behind landmark breakthroughs including Deligne’s proof of the Weil conjectures and Wiles’s proof of Fermat’s Last Theorem.

Yet as the subject expanded, its foundational literature grew vast, scattered across thousands of pages of dense monographs and seminars, much of it written in French. A great deal of the subject's working knowledge also lived as unwritten folklore passed down from advisor to student. Even defining an algebraic stack, a geometric space capable of remembering the internal symmetries of the objects it parametrizes, requires a formidable tower of prerequisites spanning commutative algebra, topologies, sheaves, and cohomology. Mathematicians needed a unified, self-contained reference where those prerequisites were written down in full detail.

In 2005, de Jong set out to organize those foundations the way software engineers maintain an open-source project like the Linux kernel. What began as an accessible introduction to algebraic stacks evolved into a living, collaborative encyclopedia comprising thousands of permanent four-character tags. The Stacks Project operates on rigorous editorial principles: every theorem carries a proof, every assumption is stated explicitly, and every step points back to the exact tags on which it depends. In doing so, de Jong and his collaborators anticipated the architecture of formal proof libraries, demonstrating that mathematics becomes far easier to verify and extend when its components have stable identifiers and explicit dependency graphs. Translating the Stacks Project into Lean brings mechanical verification to that human-designed architecture.

On October 27, 2026, Axiom released our Lean formalization of the Classification of Finite Simple Groups (CFSG). While CFSG and the Stacks Project are both monumental in scale, they represent fundamentally different engineering challenges. CFSG is organized around a single landmark theorem. The Stacks Project, by contrast, is a foundational library: its value lies in thousands of interlocking definitions, constructions, and lemmas designed to be reused across countless future proofs.

With this library, a mathematician or AI agent formalizing a new theorem about families of curves no longer needs to reconstruct the foundations of schemes or coherent cohomology from scratch. They can import the relevant definitions and theorems directly, while Lean’s kernel guarantees that every cited result is applied only when its exact hypotheses are satisfied. Formalizing the Stacks Project as one connected codebase gives researchers and agents a common chain of verified definitions and theorems on which to build, something no collection of isolated proof scripts can provide.

To make our library easy to navigate, our release preserves the permanent tag structure of the original text. At stacks.axiommath.ai, readers can view the pages of the original Stacks Project side-by-side with the corresponding Lean code and explore the interactive dependency graph. Because a single Stacks tag often unfolds into multiple formal definitions and lemmas, some newly defined and others bridged directly to existing declarations in Mathlib, our interface tracks these mappings explicitly so researchers can see precisely how the informal and formal developments align.

A smorgasbord of independently verified proofs does not make a usable mathematical library. If thousands of AI agents formalize theorems in parallel without architectural coordination, two agents will inevitably prove correct theorems about the same mathematical object using subtly incompatible definitions, or duplicate foundational infrastructure that already exists in Mathlib. Lean’s kernel will accept both files in isolation, but their results will be painfully difficult to compose downstream. Building coherent formal infrastructure requires keeping every definition and interface aligned across the entire project.

At this scale, formalization is as much systems engineering as it is mathematics. To build a single, unified library, our 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, all while keeping definitions, typeclass interfaces, and mathematical abstractions aligned across chapters.

In a tightly interconnected dependency graph of definitions and theorems, an unfaithful or trivialized formalization is quickly exposed. Ensuring that each formal statement faithfully captures the mathematical meaning of the original text is even more important than verifying its proof. Across the library, statement faithfulness is enforced automatically at scale through multi-agent auditing, semantic cross-checks against the source text, and the strict requirement that every definition and lemma must successfully interface with the downstream theorems that depend on it. Combined with targeted audits on foundational definitions and landmark theorems, this automated verification pipeline ensures that the formal library remains faithful to the mathematics of the Stacks Project.

Over the course of the project, our system surfaced dozens of statements in the Stacks Project that required local refinement, including missing hypotheses, edge cases in positive characteristic, and claims that did not hold in the full generality stated. Rather than treating failed proof attempts as mere obstacles, our agents diagnosed the underlying mathematical obstructions and constructed explicit counterexamples to prove where the original statements broke down.

Once an obstruction was isolated, the system worked to repair the mathematics so downstream chapters could still depend on it. For local oversights, our agents identified the exact missing hypotheses and formalized the corrected theorems alongside their counterexamples. Where a false supporting lemma created 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. Together, these resolutions show how large-scale formalization can actively refine and strengthen the mathematical literature itself.

Ultimately, the mathematics inside this library is the product of generations of human creativity, from the geometric intuition of the early pioneers, to the structural revolutions of Noether and Grothendieck, to the open-source scholarship of the Stacks Project and Mathlib communities. Each generation inherited a body of mathematical knowledge, cast it into a sharper language, and handed the next generation a stronger foundation. We see this formalization as part of that ongoing tradition: both a tribute to the mathematicians who built modern algebraic geometry, and working infrastructure for an emerging era in which humans and AI agents explore new mathematical frontiers together.

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 an active, living text under the stewardship of Johan de Jong and its community of contributors, while this Lean formalization is an independent open-source project maintained by Axiom. We fully respect that boundary: we keep our formalization, counterexamples, and refinements in our own repository, where mathematicians can review and draw upon them on their own terms.

You can explore the side-by-side text, inspect counterexamples, and trace the full dependency graph at stacks.axiommath.ai. Like the Stacks Project itself, our formalization is open source and designed to grow over time. We invite mathematicians, Lean developers, and AI agents to examine the library, refine its abstractions, and build new mathematics upon it.