Fomin–Williams–Zelevinsky, Chapters 1–7, in Lean 4
Mutation playground
Play with the objects the formalization is about: mutate quivers, flip triangulations, and watch exact Laurent polynomials appear. Every toy links to the formalized statements in the blueprint and to their Lean declarations.
Toy 1
Quiver mutation
A quiver is a finite directed multigraph without loops or oriented 2-cycles, with some vertices declared frozen (squares) and no arrows between two frozen vertices. Mutation at a mutable vertex \(k\) adds an arrow \(i \to j\) for every path \(i \to k \to j\) (unless \(i, j\) are both frozen), reverses the arrows at \(k\), and cancels 2-cycles. On the extended exchange matrix this is \(b'_{ij} = -b_{ij}\) if \(k \in \{i,j\}\), and \(b'_{ij} = b_{ij} + \operatorname{sgn}(b_{ik})\,[b_{ik}b_{kj}]_+\) otherwise.
Toy 2
Triangulations and flips
The quiver \(Q(T)\) of a triangulation \(T\) of a convex \(m\)-gon has a vertex for every diagonal of \(T\) (mutable) and every side (frozen). In each triangle, read the boundary clockwise: an arrow goes from each side of the triangle to the next one (omitted between two sides of the polygon). Flipping a diagonal \(\gamma\) replaces it by the other diagonal \(\gamma'\) of the quadrilateral formed by its two triangles, and \(Q(T')\) is the mutation of \(Q(T)\) at \(\gamma\).
Toy 3
Cluster variables and the Laurent phenomenon
Every cluster variable is an integer Laurent polynomial in the extended cluster (the cluster variables and the frozen variables) of any fixed seed, even though each exchange relation \(x_k x_k' = \prod_i x_i^{[b_{ik}]_+} + \prod_i x_i^{[-b_{ik}]_+}\) divides by \(x_k\). Below the divisions are carried out exactly; they never leave a remainder.
(a) Rank two
For \(B = \left[\begin{smallmatrix}0 & b\\ -c & 0\end{smallmatrix}\right]\) with \(b, c\) both positive (or both zero), alternating mutations produce the sequence \(z_{k+1} = (z_k^{e_k}+1)/z_{k-1}\), where \(e_k = c\) for even \(k\) and \(e_k = b\) for odd \(k\); its terms are the cluster variables. Each \(z_k\) is computed here as an exact Laurent polynomial in \(z_1, z_2\) (big-integer coefficients, exact polynomial division). The sequence is periodic exactly when \(bc \le 3\), with period 4, 5, 6, 8 for \(bc = 0, 1, 2, 3\).
(b) Markov triples
The Markov quiver gives exchange relations \(x_k x_k' = x_i^2 + x_j^2\). Specializing the initial cluster to \((1,1,1)\) turns the cluster variables into the Markov numbers: each move \(\nu_k\) replaces \(a_k\) by \((a_i^2+a_j^2)/a_k\), which on a Markov triple equals \(3a_ia_j - a_k\); it preserves \(a_1^2+a_2^2+a_3^2 = 3a_1a_2a_3\), and every positive solution of this equation is reached from \((1,1,1)\).
(c) Somos-4
The recurrence \(z_{t+4}z_t = z_{t+3}z_{t+1} + z_{t+2}^2\) with \(z_0=z_1=z_2=z_3=1\) divides at every step, yet produces only integers. Its terms are cluster variables: mutating the Somos-4 quiver (a preset in Toy 1) at vertex 1 rotates it, so the mutations at \(1,2,3,4,1,2,\dots\) all have the Somos-4 exchange relation, and the Laurent phenomenon gives integrality.
Toy 4
Plabic graphs and square moves
A plabic graph is a planar graph in a disk whose internal vertices are coloured black or white. Its quiver \(Q(G)\) has a vertex for each face (faces touching the boundary are frozen) and, for every edge joining a white and a black vertex, an arrow across it between the two faces it separates (none if both are boundary faces), oriented so that the white endpoint is on the left of the arrow; then 2-cycles cancel. A square move swaps the colours of the four trivalent vertices around a square face: it mutates \(Q(G)\) at that face and keeps the trip permutation. Shown here is the graph \(G(T)\) of a triangulation, whose quiver is \(Q(T)\).