Cluster Algebras, Formalized in Lean

Today, Axiom is releasing a library of formally verified mathematics based on the first seven chapters of Introduction to Cluster Algebras, by Sergey Fomin, Lauren Williams, and Andrei Zelevinsky. We have written its definitions and arguments in Lean, a language and proof-checking system. The book is freely available in four parts: Chapters 1–3, 4–5, 6, and 7.

Lean checks that each proof establishes its conclusion from the assumptions listed in the theorem. The library gives researchers a collection of precise statements on which to build.

Sergey Fomin and Andrei Zelevinsky developed cluster algebras in a series of four foundational papers published between 2002 and 2007; Arkady Berenstein joined them for the third. Their starting questions came from algebra and the study of symmetry. The central operation is called mutation. One starts with a collection of variables called a cluster. One can then replace one of the variables with a new variable that is calculated according to a particular rule. After repeating this process, one obtains several (possibly infinitely many) variables, which sometimes encode deep facts about geometry or algebra. Cluster algebras have now taken on a life of their own. Researchers have found that they appear in a remarkable number of settings throughout math, and they even have important connections to physics.

Fomin and Zelevinsky started by studying deep algebraic structures called canonical bases. This led them to find specific examples of what they would then develop into a broad theory. What makes the general theory so beautiful and compelling is that it encompasses numerous examples of systems that people had already studied in isolation. Moreover, there are general truths that one can prove about all cluster algebras, thereby explaining and unifying phenomena that had previously been seen as strange, one-off miracles.

Here is a basic example. In the 1980s, Michael Somos studied a sequence starting with 1, 1, 1, 1. At each step, we look at the previous four terms in the sequence and call them $a$, $b$, $c$, and $d$, in order. The next term in the sequence is

$$\frac{b \times d + c^2}{a}.$$

For example, the fifth number in the sequence is

$$\frac{1 \times 1 + 1^2}{1},$$

which is 2. The sixth number is

$$\frac{1 \times 2 + 1^2}{1},$$

which is 3. The seventh number is

$$\frac{1 \times 3 + 2^2}{1},$$

which is 7. The first several terms in the sequence are

$$1, 1, 1, 1, 2, 3, 7, 23, 59, 314, 1529, 8209, \ldots$$

These are all whole numbers! To see why this is astounding, consider that the number 8209 was computed as

$$\frac{59 \times 1529 + 314^2}{23}.$$

It’s remarkable that the number $59 \times 1529 + 314^2$, which is 188807, happens to have 23 as a factor!

This sequence is called the Somos-4 sequence because it starts with four 1s and uses a rule in which the next number is always computed using the previous four numbers. It is just one of the amazing sequences discovered by Somos. The others, which are defined by similar rules, are the Somos-5, Somos-6, and Somos-7 sequences.

It turns out that the Somos-4 sequence (as well as the Somos-5 sequence) can be constructed from a cluster algebra. Fomin and Zelevinsky proved a remarkable fact known as the Laurent Phenomenon. Roughly speaking, this says the following. Suppose one starts with a collection of variables and then repeatedly mutates the variables in the fashion they described. After doing this for some time, one can take one of the new variables and express it in terms of the original variables. This expression will take the form $P/Q$, where each of $P$ and $Q$ is obtained by adding, subtracting, and multiplying some of the original variables. The Laurent Phenomenon says that one can choose $P$ and $Q$ so that $Q$ is just a product of the original variables raised to some integer powers, with no addition or subtraction at all.

In the very special case of the Somos-4 sequence, the initial variables are the four starting numbers, which are just 1, 1, 1, 1. The new variables obtained through mutation are just the later terms in the sequence, so each such term can be expressed as $P/Q$, where $P$ is obtained by adding, subtracting, and multiplying the initial four 1s. Note that this means $P$ is an integer. The Laurent Phenomenon says that $Q$ is just a product of the initial 1s raised to some integer powers. But 1 raised to any power is 1, and a product of a bunch of 1s is 1. This means $Q = 1$, so $P/Q$ is just $P$, which is a whole number! Thus, the Laurent Phenomenon explains the miracle of the Somos-4 sequence.

Each cluster algebra has its own collection of rules governing how mutations are performed. One can specify these rules by choosing a directed graph with no 1-cycles or 2-cycles. In other words, this is a set of nodes together with a set of arrows, where each arrow points from one node to a different node, and no two arrows between the same pair of nodes point in opposite directions. This directed graph is called a quiver because it has arrows.

Another example of a cluster algebra relates to an equation studied by Andrey Markov in 1879:

$$x^2 + y^2 + z^2 = 3xyz.$$

In number theory, there is a great deal of interest in triples $(x, y, z)$ of positive whole numbers that satisfy this equation. These are called Markov triples. Some examples include $(1, 1, 1)$, $(1, 1, 2)$, and $(1, 2, 5)$. From any solution, one can choose an entry and replace it by three times the product of the other two minus the chosen entry. This gives another solution. For example, starting with $(1, 2, 5)$, we can replace the 2 by $3 \times 1 \times 5 - 2$, which is 13, to obtain the new triple $(1, 5, 13)$. Every Markov triple can be reached from $(1, 1, 1)$ by repeating these operations.

It turns out that this process for changing one Markov triple into another comes from mutation in a certain cluster algebra. The quiver defining this cluster algebra has three nodes $x$, $y$, $z$, with two arrows from $x$ to $y$, two arrows from $y$ to $z$, and two arrows from $z$ to $x$.

A tantalizing question, associated with Frobenius’s work in 1913, remains open: does the largest number in a Markov triple determine the other two, apart from their order?

Some cluster algebras contain infinitely many different variables, while others contain only finitely many. Fomin and Zelevinsky classified the finite cases in work published in 2003. Their basic building blocks fall into four families and five exceptional types. This is the same list that appears in an older classification from the mathematics of symmetry.

One exceptional type, called $E_8$, has 128 different cluster variables arranged into 25,080 collections, or clusters, each containing eight variables. The library includes a calculation of these counts checked directly by Lean.

The seventh chapter of the book studies networks drawn inside a circle. Their edges do not cross, each interior vertex is black or white, and each numbered boundary vertex has one edge leading into the network. Each connected piece reaches the boundary. These are called plabic graphs. Alexander Postnikov introduced them to study remarkable geometric spaces called totally nonnegative Grassmannians. For suitable graphs, the regions between the edges represent variables used to describe those spaces. The internal regions supply the changing variables in a cluster; the regions touching the boundary supply quantities held fixed. Trips, which are certain paths that walk along the edges of the graph, determine the labels of the regions. In the example below, each label is a set of three numbers.

For the graphs used here to represent clusters, a square move swaps the colors of four alternating black and white corners, each with three incident edges. This changes one cluster variable. In the four-boundary-point example below, the central label changes from 24 to 13.

These diagrams connect to Scott’s theorem about Grassmannians, which are geometric spaces whose points represent lines, planes, or higher-dimensional subspaces of a fixed space. Scott showed that the algebra built from their standard coordinates has a cluster algebra structure.

The chapter also classifies graphs satisfying certain simplifying conditions. Two such graphs are connected by the allowed local moves precisely when their trips give the same boundary connections, including the color marker for any trip returning to its starting point.

Cluster algebras have helped prove predictions about repeating patterns in mathematical models of quantum physics. In 1991, Alexei Zamolodchikov proposed a periodicity conjecture for certain systems of equations. Fomin and Zelevinsky proved a version in work published in 2003; Bernhard Keller later established a broader version, published in 2013.

Another connection concerns calculations of how particles scatter. In an idealized model of particle interactions, Nima Arkani-Hamed and collaborators related these calculations to diagrams built from black and white vertices. The same local moves used for plabic graphs help organize the calculations. Other researchers found that coordinates built from products and ratios of cluster variables help describe particular six- and seven-particle calculations.

Yuji Kodama and Lauren Williams also used this mathematics to describe certain solutions of the KP equation, a model used to study shallow-water waves. Graphs related to the ones above organize the patterns formed by interacting solitary waves in these solutions.

These applications show where the mathematics is used. Our library covers the underlying textbook material; formalizing these physics results would be a separate project.

Axiom’s work translates definitions and arguments from the book into Lean 4, building on Mathlib, the community’s library of formalized mathematics. A formal proof must supply enough detail for Lean to check each logical step. Results already in the library can then be used in later proofs.

Computer checking and mathematical review serve different purposes. Lean checks whether a conclusion follows from its stated assumptions. Mathematicians must also check whether the formal definitions and statements express the mathematics intended by the book. Both are needed for a useful formalization.

Some results that the book uses from elsewhere, including the classification of symmetry types, remain explicit assumptions, as do selected exercises. The library records these as hypotheses in the relevant theorems rather than adding new axioms to Lean. Other exercises are outside the published scope. A checked proof therefore establishes exactly the statement written in Lean, including its hypotheses; it does not automatically prove every mathematical fact on which that statement depends.

The source includes explanations linking the formal statements to the book. Readers can inspect individual results, trace their dependencies, and see which assumptions they use. This makes both the coverage and its limitations available for review.

The first seven chapters cover foundations of a much larger subject. There are many directions for future formalization beyond this library.

In the simplified formulas described earlier, subtraction is never actually needed: every integer coefficient is nonnegative. Kyungyong Lee and Ralf Schiffler proved this for a broad class of cluster algebras in work published in 2015. Mark Gross, Paul Hacking, Sean Keel, and Maxim Kontsevich established a more general result in a paper published in 2018, using ideas from geometry. These positivity results are outside the scope of this library.

Other directions include studying cluster algebras that come from triangulated surfaces, studying quantum versions of the theory, and developing the connections to physics. The definitions and results already formalized provide a starting point for such projects.

The library is intended for researchers and developers who want to build further mathematics in Lean. They can reuse its definitions and proofs, check the assumptions a result needs, and extend the parts relevant to their work.

We thank Sergey Fomin, Lauren Williams, and the late Andrei Zelevinsky for the book, and the Lean and Mathlib communities for the tools and mathematical library on which this work depends.

The source code is available at github.com/AxiomMath/ClusterAlgebras.

We have also created an interactive website that researchers can use to learn about cluster algebras and explore the formalization: https://clusteralgebras.axiommath.ai

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, and Chenkai Wang.