The Stacks Project, formalized in Lean
The Stacks Project is an open-source textbook and reference work on algebraic geometry. Each of its definitions, lemmas, propositions and theorems carries a stable four-character tag.
Here the tagged results are formalized as Lean definitions and proofs built on Mathlib, and Lean’s kernel checks every completed proof. Each tag links to its Lean code and its dependencies.
- Lean files
- —
- Declarations
- —
- Lines of Lean
- —
Dependency graph
?
One node per tagged Lean declaration. A level is one more dependency step between tagged declarations; tags label the declarations.
Parts → chapters → sections, sized by declaration count. Click a part, chapter or section to zoom to it, or a declaration to lay out its neighbours.
Filters & legend
Zoom level
Dependency edges
Node types
Library
?
Each entry is a tag of the Stacks Project: a definition, lemma, proposition, theorem or other item, identified by its four-character tag. When several Lean declarations carry the same tag, each formalizes a different part of it, and each has a tab above the code.
Tags in green are already in Mathlib; tags in red were judged not applicable to Lean.
Select a tag to view its Lean source and dependencies.
Statement
Lean referencesUsed in Lean byNatural-language citationsCited by
Lean references
Used in Lean by
Natural-language citations
Cited by
Contributing
We welcome contributions from anyone interested in formalizing the Stacks Project. The goal is for people to review, polish, build upon, use and adapt this code, and eventually to upstream as much of it as is reasonable to Mathlib.
How to contribute
The library, Stacks, has two parts. StacksCore is code that a person has checked against the Stacks Project and brought up to Mathlib standards. StacksFrontier is code written by AI agents that has not had that review yet. Lean checks every proof in both.
You can help in five ways:
- Formalize an open exercise, example or remark from the list below.
- Review code in
StacksFrontierand move it intoStacksCore. - Formalize a result directly for
StacksCore. - Take on one of the projects below.
- Improve an existing proof.
Claim new formalizations and reviews before you start, so that two people do not do the same thing.
- ClaimCheck the open claims, then open a claim with a blueprint: the exact statement, the Lean statement you intend to prove, the declarations in this library or in Mathlib that you will use or extend, and a proof outline. The task board pre-fills it for you.
- Get it approvedA maintainer reviews the blueprint. When it is approved, the issue is labelled
blueprint-approvedand assigned to you: that is your claim. - FormalizeWrite the Lean code with
@[stacks TAG]on the declaration, and open a pull request that closes the issue.
Improvements to existing proofs and small fixes (typos, broken proofs, documentation) need no claim: open a pull request directly. Every pull request, to either tier, is reviewed by the maintainers: Kenny Lau, Brian Nugent, Ashvin A. Swaminathan and Yunzhou Xie.
Formalization tasks
Loading tasks…
Axiom Math contributors
Rohan Aanegola†, Alberto Alfarano†, François Charton†, Evan Chen*, Ruiz Chen†, Constantin Eichenberg†, Srihari Ganesh†, Tobias Gessler†, Erik Gregory†, Leopold Haller†, Sidharth Hariharan*, Letong Hong◇, Vasily Ilin†, Albert Jiang†, Yunjiang Jiang†, Tadeusz Jordan†, Angus Joshi†, Andranik Kurghinyan†, Kenny Lau*†, Simon Mahns†, Rishi Malhotra†, Bhavik Mehta*, Michał Mogielnicki†, Brian Nugent*, Connor Olson†, Ken Ono*, Gaurang Pendharkar†, Bartosz Piotrowski†, Anish Rajeev†, Karun Ram†, Aditya Ramabadran†, Charlie Ray†, Guillaume Remy†, Shubho Sengupta◇, Alex Sorokin*, Ashvin A. Swaminathan*†, Jesse Thorner*, Aleksey Tsaplin†, Niels Voss†, Chao Wang†, Chenkai Wang†, Yunzhou Xie*, Jimmy Xin†, Tony Yue Yu*, Yinglun Zhu†
*Mathematical contributors†Engineering contributors◇Principal investigators