Stacks Project in Lean

Stacks Project in Lean is an open-source library that translates material from the Stacks Project into machine-checkable mathematics in Lean. Axiom Math announced the library on November 4, 2026, reporting about 16 million lines of code. It is built on Mathlib and organizes formal definitions and results into a connected library that other proofs can import.^[1][2]

The release has two review tiers. StacksCore contains human-reviewed formalizations, while StacksFrontier contains AI-generated formalizations awaiting that review. The project says proofs in both tiers are checked by Lean's kernel. Checking a formal proof establishes a different property from checking whether its statement faithfully translates the original mathematics, so the tiers remain an important qualification on the release.^[2][3][10]

The formalization is maintained independently of the original Stacks Project. Its release metadata identifies a particular source revision and excludes exercises and obsolete chapters. Descriptions of the release as formalizing the "entire" project therefore need to be read with these scope and review limits.^[1][3]

The source project

The original Stacks Project is a collaborative textbook and reference on algebraic geometry and algebraic stacks. Its intended readers are graduate students and researchers. Its scope includes commutative algebra, schemes, varieties and algebraic spaces, rather than an introductory treatment of mathematics.^[8]

Aise Johan de Jong initiated the project in 2005, and its first source-code commit dates to May 2008. The text assigns permanent tags to results, allowing a proof to refer to a particular definition or lemma even as chapter numbering and presentation change.^[8]

These identifiers also connect the informal text to the Lean library. A source result can correspond to several formal declarations, and some material is already covered by Mathlib. The formalization records these relationships rather than assuming a one-to-one correspondence between a textbook tag and a Lean theorem.^[2][7]

Release and coverage

The public release linked from Axiom's project website is commit f8e70c5dd04bfabcb423d5e325461f527c85a5d6 of the AxiomMath/Stacks repository.^[2][7] Its technical metadata separates the source being formalized from the version of the tools used to formalize it.

The source snapshot, coverage and review status come from the release's formalization.yaml; the toolchain and dependency versions are specified separately in lean-toolchain, lakefile.toml and the dependency manifest.^[3][5][6] The line and module counts are publisher-reported scale measures, not independent measures of mathematical correctness.^[1][2]

The README describes coverage of tags with formalizable content, while also listing remaining examples, exercises and remarks as contribution opportunities. Together with the explicit exclusions in the metadata, this means the release should not be interpreted as a reviewed translation of every sentence or every exercise in every later revision of the living source text.^[2][3]

Human and AI contributions

Axiom describes an engineering process in which coordinated agents translated statements, searched for existing abstractions, produced proofs and resolved dependencies. The repository metadata identifies the company's AxiomProver system as an automated method alongside manual work. It says foundational definitions and StacksCore were formalized and reviewed by people, while most of StacksFrontier was formalized autonomously.^[1][3]

The distinction between the two tiers concerns review, not whether one tier is intended to contain incomplete proof placeholders.

The release metadata labels its review status self-assessed. It names Kenny Lau, Brian Nugent, Ashvin A. Swaminathan and Yunzhou Xie as responsible maintainers. Its contribution guide requires review of pull requests to either tier; that process does not mean all previously released Frontier material has already received the Core tier's review.^[3][4]

Tags, dependencies and reuse

A declaration can carry @[stacks TAG] to identify the source item it formalizes. If it formalizes only part of an item, the attribute can include a comment identifying that part. When Mathlib already provides the result, add_to_stacks records the mapping on the existing declaration.^[2]

The library also records references to numbered results in Grothendieck's Éléments de géométrie algébrique (EGA) and Séminaire de géométrie algébrique (SGA). Those annotations distinguish an entire result, a more general result, selected clauses or a special case. A reference is therefore not automatically a claim that the full corresponding EGA or SGA item has been formalized in its original generality.^[2]

The website provides a library browser and dependency graph. These connect source tags to Lean statements, code and dependencies. A tag may have several associated declarations, which the interface presents separately. This is useful when a single informal lemma requires multiple formal constructions or intermediate results.^[7]

The reusable-library approach builds on Mathlib's existing hierarchy of mathematical structures. The academic description of Mathlib emphasizes its unified library, classical mathematics, automation and community organization. That work provides background for the infrastructure used by Stacks, rather than independent validation of this particular release.^[12]

What proof checking establishes

Lean represents a theorem as a formal statement with a proof term. Its kernel checks that the proof has the required type. A proof-generating agent or tactic can propose the term, but the checker is responsible for accepting it under the system's rules. Lean 4 also provides a programming language and extensible automation infrastructure around that core.^[10][13]

Two checks remain distinct:

For example, proving a weaker statement is not sufficient to formalize a stronger textbook statement. The contribution guide explicitly prohibits weakening a result simply to make it provable and directs contributors to report a source statement they believe is wrong.^[4]

The project prohibits sorry, admit, native_decide and new axiom declarations in contributions. Its metadata reports zero sorry uses, including in definitions, and lists propext, Classical.choice and Quot.sound as the axioms used.^[3][4] These are the three standard mathematical axioms identified by Lean's validation guidance.^[10][11]

Those declarations are project reports and contribution requirements, not an independent rebuild of all released modules. Lean's own documentation recommends inspecting transitive axiom dependencies with #print axioms; it also describes rechecking compiled proofs with lean4checker for additional assurance. Its guidance still conditions trust on the formal statement matching the intended informal meaning.^[10]

Building and inspecting the library

The README gives the following build commands:^[2]

lake exe cache get
lake build

The first command obtains compiled Mathlib files. At the release snapshot, the README warns that compiling the Stacks library itself takes substantial time and memory because it contains about 63,000 modules. A cache for compiled Stacks modules is described as planned, not as an already available feature.^[2]

The project documents these Lean commands for exploring its mappings and assumptions:^[2][4]

import Stacks

#stacks_tags
#stacks_tags!

import Stacks loads both review tiers. #stacks_tags lists tagged declarations, while #stacks_tags! includes their statements. The separate #print axioms command can be applied to a particular declaration to inspect what it depends on.^[2][10]

The release's compiler and Mathlib revision are pinned. Those pins identify the environment documented for the release; they should not be replaced by an assumption that an arbitrary later Lean or Mathlib version is interchangeable.^[5][6]

Relationship to the original maintainers

Axiom's library and the original Stacks Project have separate maintainers and contribution processes. On October 21, 2026, de Jong asked that AI-generated comments and pull requests not be submitted to the original project for the time being. He said he intended to continue maintaining and correcting the text by hand.^[9]

Axiom's announcement acknowledges that request and says its formalizations, proposed corrections and counterexamples are kept in its own repository. It reports finding statements needing refinement, but that is a claim from the formalization's publisher, not evidence that the original maintainers accepted those proposed corrections.^[1]

The library's Apache 2.0 license is also distinct from the GNU Free Documentation License that its README identifies for the original Stacks Project text.^[2][14]

Limitations

The release provides a public, inspectable artifact and a path for further review. Its published scope, self-assessed review status and split between Core and Frontier matter when deciding what has been established. Axiom's automated semantic checks and dependency integration do not remove the need to inspect whether each formal statement matches its source.^[1][3][10]

A large codebase is not by itself a benchmark of an AI system's ability to discover new mathematics. The source reference and much of the supporting infrastructure were developed by mathematicians and the Lean community. The release is primarily a formalization and software-library project; evaluating any proposed new theorem or correction requires examining that result and its proof separately.^[1][8][12]

References

1. ^1 ^2 ^3 ^4 ^5 ^6 ^7Axiom Math. The Stacks Project, formalized in Lean. Release announcement, November 4, 2026.
2. ^1 ^2 ^3 ^4 ^5 ^6 ^7 ^8 ^9 ^10 ^11 ^12 ^13Axiom Math. Stacks README. Release commit `f8e70c5dd04bfabcb423d5e325461f527c85a5d6`, checked November 5, 2026.
3. ^1 ^2 ^3 ^4 ^5 ^6 ^7 ^8Axiom Math. Stacks formalization metadata. Source snapshot, scope, review and automation declarations, checked November 5, 2026.
4. ^1 ^2 ^3 ^4Axiom Math. Stacks contribution guide. Checked November 5, 2026.
5. ^1 ^2Axiom Math. Stacks Lake configuration and dependency manifest. Checked November 5, 2026.
6. ^1 ^2Axiom Math. Stacks Lean toolchain. Checked November 5, 2026.
7. ^1 ^2 ^3Axiom Math. Stacks Project in Lean website. Library browser, dependency graph and contribution overview, checked November 5, 2026.
8. ^1 ^2 ^3The Stacks Project authors. About the Stacks Project. Scope, history and maintenance, checked November 5, 2026.
9. ^Johan de Jong. No AI for now. Stacks Project Blog, October 21, 2026.
10. ^1 ^2 ^3 ^4 ^5 ^6Lean contributors. Validating a Lean Proof. Lean Language Reference, checked November 5, 2026.
11. ^Lean contributors. Axioms. Lean Language Reference, checked November 5, 2026.
12. ^1 ^2The mathlib Community. The Lean Mathematical Library. *Certified Programs and Proofs*, 2020. DOI: 10.1145/3372885.3373824.
13. ^Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language. *Automated Deduction*, 2021. DOI: 10.1007/978-3-030-79876-5_37.
14. ^Axiom Math. Stacks license. Apache License 2.0, checked November 5, 2026.