Lean formalization of
Introduction to Cluster Algebras
An interactive, dependency-aware blueprint of Chapters 1–7 of Fomin, Williams, and Zelevinsky’s Introduction to Cluster Algebras. Every definition, lemma, and theorem comes with its status, the results it uses, a proof, and links to the Lean declarations.
How to use this page
- Pick a chapter with the numbered buttons or the table of contents; the address bar always holds a link to what you are reading.
- Hover over (or focus, or long-press) any cross-reference to preview the statement it points to.
- Press / to search by number (
7.6.9,3.4), title, label (thm_laurent), or Lean name; Enter jumps to the result. - Filter by status or kind, expand every proof at once, and follow Show in graph to see an entry in the dependency graph.
Loading the blueprint…