# Stacks Project in Lean

> Source: https://aiwiki.ai/wiki/stacks_project_in_lean
> Updated: 2026-11-05
> Categories: AI Research, AI for Science, Mathematics, Open Source AI
> License: CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/) - attribute to "AI Wiki (aiwiki.ai)"
> Cite as: AI Wiki. "Stacks Project in Lean." aiwiki.ai, 5 Nov 2026. https://aiwiki.ai/wiki/stacks_project_in_lean
> From AI Wiki (https://aiwiki.ai), the free encyclopedia of artificial intelligence. Reuse freely with attribution.

**Stacks Project in Lean** is an open-source library that translates material from the Stacks Project into machine-checkable mathematics in [Lean](https://aiwiki.ai/wiki/lean). [Axiom Math](https://aiwiki.ai/wiki/axiom_math) announced the library on November 4, 2026, reporting about 16 million lines of code. It is built on [Mathlib](https://aiwiki.ai/wiki/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.

| Item | Release documentation |
| --- | --- |
| Library | `Stacks`, with `StacksCore` and `StacksFrontier` as its two tiers |
| Source snapshot | Stacks Project commit `a5811b23a9bfc23256ca49035d7e121533dd6f29` |
| Stated source coverage | Chapters 1-109; exercises and obsolete chapters are outside the metadata's scope |
| Lean toolchain | `leanprover/lean4:v4.34.0-rc2` |
| Mathlib dependency | Commit `16edf57de7933555826307a3d81b4391a3657a09` |
| Lake package version | `0.1.0` |
| Scale | About 16 million lines according to Axiom's announcement; about 63,000 modules according to the repository README |
| Library license | Apache License 2.0 |

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](https://aiwiki.ai/wiki/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.

| Tier | Project description | Review boundary |
| --- | --- | --- |
| `StacksCore` | Formalizations checked against the Stacks Project and brought to Mathlib conventions for naming, generality and style | Human review of correspondence to the source is part of this tier's stated standard |
| `StacksFrontier` | Drafted formalizations, including work written by AI agents | The metadata reports successful builds and standard-axiom checks, but says human review is still pending |

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:

| Question | Relevant check |
| --- | --- |
| Does the proof establish the formal statement under its assumptions? | Kernel checking and inspection of the proof's dependencies and axioms |
| Does the formal statement express the intended source result? | Review of definitions, hypotheses, quantifiers and correspondence with the source text |

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]

```bash
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]

```lean
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]

## See also

- [Automated Theorem Proving](https://aiwiki.ai/wiki/automated_theorem_proving)
- [Mathematical Reasoning in AI](https://aiwiki.ai/wiki/mathematical_reasoning)

## References

1. Axiom Math. [The Stacks Project, formalized in Lean](https://axiommath.ai/research/the-stacks-project-formalized/). Release announcement, November 4, 2026.
2. Axiom Math. [Stacks README](https://github.com/AxiomMath/Stacks/blob/f8e70c5dd04bfabcb423d5e325461f527c85a5d6/README.md). Release commit `f8e70c5dd04bfabcb423d5e325461f527c85a5d6`, checked November 5, 2026.
3. Axiom Math. [Stacks formalization metadata](https://github.com/AxiomMath/Stacks/blob/f8e70c5dd04bfabcb423d5e325461f527c85a5d6/formalization.yaml). Source snapshot, scope, review and automation declarations, checked November 5, 2026.
4. Axiom Math. [Stacks contribution guide](https://github.com/AxiomMath/Stacks/blob/f8e70c5dd04bfabcb423d5e325461f527c85a5d6/CONTRIBUTING.md). Checked November 5, 2026.
5. Axiom Math. [Stacks Lake configuration](https://github.com/AxiomMath/Stacks/blob/f8e70c5dd04bfabcb423d5e325461f527c85a5d6/lakefile.toml) and [dependency manifest](https://github.com/AxiomMath/Stacks/blob/f8e70c5dd04bfabcb423d5e325461f527c85a5d6/lake-manifest.json). Checked November 5, 2026.
6. Axiom Math. [Stacks Lean toolchain](https://github.com/AxiomMath/Stacks/blob/f8e70c5dd04bfabcb423d5e325461f527c85a5d6/lean-toolchain). Checked November 5, 2026.
7. Axiom Math. [Stacks Project in Lean website](https://stacks.axiommath.ai/). Library browser, dependency graph and contribution overview, checked November 5, 2026.
8. The Stacks Project authors. [About the Stacks Project](https://stacks.math.columbia.edu/about). Scope, history and maintenance, checked November 5, 2026.
9. Johan de Jong. [No AI for now](https://www.math.columbia.edu/~dejong/wordpress/?p=5033). Stacks Project Blog, October 21, 2026.
10. Lean contributors. [Validating a Lean Proof](https://lean-lang.org/doc/reference/latest/ValidatingProofs/). Lean Language Reference, checked November 5, 2026.
11. Lean contributors. [Axioms](https://lean-lang.org/doc/reference/latest/Axioms/). Lean Language Reference, checked November 5, 2026.
12. The mathlib Community. [The Lean Mathematical Library](https://leanprover-community.github.io/papers/mathlib-paper.pdf). *Certified Programs and Proofs*, 2020. DOI: [10.1145/3372885.3373824](https://doi.org/10.1145/3372885.3373824).
13. Leonardo de Moura and Sebastian Ullrich. [The Lean 4 Theorem Prover and Programming Language](https://lean-lang.org/papers/lean4.pdf). *Automated Deduction*, 2021. DOI: [10.1007/978-3-030-79876-5_37](https://doi.org/10.1007/978-3-030-79876-5_37).
14. Axiom Math. [Stacks license](https://github.com/AxiomMath/Stacks/blob/f8e70c5dd04bfabcb423d5e325461f527c85a5d6/LICENSE). Apache License 2.0, checked November 5, 2026.