Stacks Project 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. 40,433 tagged Lean declarations in 35 dependency levels. One node per tagged Lean declaration. Depth counts Lean dependencies between tagged declarations, including those that pass through at most three untagged helper declarations; natural-language citations have their own edge colours. The ground is the chapter treemap. Each declaration is a column as tall as its dependency level. The book’s Theorems are gold and its Propositions blue, one column per Stacks tag. Drag to turn it. Lemma Rests on a chain of 9 tagged Lean declarations Tags: 082X, 082Y Chapter 67, Morphisms of Algebraic Spaces 000I001B001I001M001N007U00V2