A formalization of Chapters 1–7 of Fomin, Williams, and Zelevinsky’s textbook, from total positivity and quiver mutation to the finite type classification, cluster structures in commutative rings, and plabic graphs.
Core contributors: Colin Defant*, Alex Sorokin*
Other contributors: Rafael Cabral†, Dean Cureton*†, Erik Gregory†, Aaron Hill†, Letong Hong◇, Qinheping Hu†, Vasily Ilin†, Dustin Jamner†, Albert Jiang†, Tadeusz Jordan†, Andranik Kurghinyan†, Kenny Lau*†, Jonathan Laurent†, David Liang†, Jannis Limperg†, Simon Mahns†, Bhavik Mehta*†, Brian Nugent*, Connor Olson†, Ken Ono*‡, Eric Paul†, Dhruv Rajan†, Karun Ram†, Charlie Ray†, Ho Chung Siu†, Ashvin A. Swaminathan*†, Jesse Thorner*, Aleksey Tsaplin†, Niels Voss†, Chenkai Wang†
Cluster algebras were introduced by Fomin and Zelevinsky in 2002. A cluster algebra is a commutative ring generated by a distinguished set of cluster variables, grouped into overlapping clusters and produced from an initial seed by a combinatorial process called mutation. Since then they have turned up in total positivity, representation theory, Teichmüller theory, Poisson geometry, and the combinatorics of the Grassmannian.
Fomin, Williams, and Zelevinsky’s Introduction to Cluster Algebras develops the theory from first principles. This project formalizes its first seven chapters in Lean 4, on top of Mathlib, statement by statement in the book’s order:
The interactive blueprint breaks the seven chapters into definitions, lemmas, propositions, and theorems. Each entry has a precise statement, the earlier results it uses, a proof, and links to the Lean declarations that formalize it; the dependency graph shows how they fit together.
The Lean code is the library ClusterAlgebras, in the public repository
AxiomMath/ClusterAlgebras. Its challenge file restates eleven headline
theorems, among them the finite type classification, and Lean’s comparator checks that the
library proves exactly those statements.
The Lean library declares no axioms. Its assumptions are stated as hypotheses, marked Assumed in the blueprint: each is a Lean proposition, and every result that rests on one takes it as an explicit hypothesis, so its statement shows what it assumes. They are of two kinds: results the book cites from the literature, such as the Cartan–Killing classification, and exercises the book leaves to the reader. Some exercises were proved anyway (6 of them, marked “Exercise, proved”). The Excluded entries are exercises, and nodes needed only for them, whose solutions the project deliberately does not publish.
A few of the theorems in the library, with their statements as in the blueprint. Hover over a reference to preview it.
Chapter 3 · Theorem 3.4.13
The headline result of Chapter 3, with its sharpening that frozen variables do not appear in denominators. Its number-theoretic applications are formalized too: Markov triples, Euler’s factor of \(2^{32}+1\), Somos-4, and the Fordy–Marsh recurrences.
Chapter 5 · Theorem 5.10.42
Finite type is matched with the Cartan–Killing types, one theorem per type:
An,
Bn,
Cn,
Dn,
E6,7,8,
F4,
G2.
For E8, the 128 cluster
variables and 25,080 clusters are certified by a computation checked by Lean’s kernel, without
native_decide.
Chapter 6 · Theorem 6.4.25
Scott’s theorem: the homogeneous coordinate ring of the Grassmannian is a cluster algebra. Like the cluster structures on \(\mathbb C[\mathrm{SL}_k]^U\), \(\mathbb C[\mathrm{Mat}_{k\times k}]\), and \(\mathbb C[\mathrm{SL}_k]\), it is proved through the Starfish lemma.
Chapter 7 · Theorem 7.7.36
Two reduced plabic graphs are move-equivalent exactly when they have the same decorated trip permutation. Along the way: reduced ⇔ minimal triple diagram, the bad features criterion, and the resonance criterion.
The book has appeared on the arXiv in four parts. The blueprint follows them chapter by chapter, in the book’s order; the opening section of each chapter in the blueprint records exactly what is in scope and how cited results and exercises are treated.
Total positivity, mutations of quivers and matrices, and clusters and seeds, up to the Laurent phenomenon and Y-patterns.
New patterns from old (restriction, freezing, changing coefficients, folding) and the classification of seed patterns of finite type.
Cluster structures in commutative rings: the Starfish lemma; the cluster structures on \(\mathbb C[\mathrm{SL}_k]^U\), Plücker rings, \(\mathbb C[\mathrm{Mat}_{k\times k}]\), and \(\mathbb C[\mathrm{SL}_k]\); and presentations by generators and relations.
Plabic graphs: trips and reduced graphs, triple diagrams, the bad features and resonance criteria, affine permutations, bridge decompositions, and edge and face labels.
We first wrote the book as a blueprint, with a separate entry for each definition and result. The dependency graph then gave an order in which to formalize it.
Give every definition, lemma, and theorem a label, a precise statement, and the list of earlier results it uses, following the book chapter by chapter. Mathematicians decided what is in scope, which cited results are assumed, and how exercises are treated.
AI agents (Anthropic’s Claude), working with Axiom Math’s AxiomCode tooling, formalized the blueprint entry by entry in Lean 4 on top of Mathlib. Every proof is checked by Lean’s kernel and uses only Lean’s standard axioms; the assumed results enter as explicit hypotheses.
The headline theorems are restated in a separate challenge file. Lean’s comparator checks, with two independent kernels, that the library proves exactly those statements using only Lean’s standard axioms.
@misc{axiom-cluster-algebras,
author = {Defant, Colin and Sorokin, Alex and Cabral, Rafael and Cureton, Dean and Gregory, Erik and Hill, Aaron and Hong, Letong and Hu, Qinheping and Ilin, Vasily and Jamner, Dustin and Jiang, Albert and Jordan, Tadeusz and Kurghinyan, Andranik and Lau, Kenny and Laurent, Jonathan and Liang, David and Limperg, Jannis and Mahns, Simon and Mehta, Bhavik and Nugent, Brian and Olson, Connor and Ono, Ken and Paul, Eric and Rajan, Dhruv and Ram, Karun and Ray, Charlie and Siu, Ho Chung and Swaminathan, Ashvin A. and Thorner, Jesse and Tsaplin, Aleksey and Voss, Niels and Wang, Chenkai},
title = {Lean formalization of {I}ntroduction to {C}luster {A}lgebras},
year = {2026},
note = {Interactive Lean formalization blueprint of Fomin, Williams, and Zelevinsky, Introduction to Cluster Algebras, Chapters 1--7}
}