Cluster algebras, all in Lean?

The claim, in plain words

This is AX08. Start with two numbers and one rule: the next number is the last one plus one, divided by the one before it. Begin with one and one. One plus one, over one, is two. Two plus one, over one, is three. Three plus one, over two, is two. Then one, and one again. We are back where we started: the sequence repeats every five steps, around a pentagon. Now use letters, x1 and x2, instead of numbers. Each new term is a fraction, and two things stand out. Every bottom is just a product of x1 and x2, never a sum. And every number on top is positive. This is our own computation, and both facts are tiny cases of general theorems.

This rule comes from one of the smallest cluster algebras, introduced by Sergey Fomin and Andrei Zelevinsky in 2002. You keep a handful of variables, called a cluster, and a diagram of arrows between them, called a quiver. One move, called mutation, swaps one variable for a new one. The new variable times the old one equals the product of the variables with arrows coming in, plus the product of those with arrows going out. Then the arrows change: every path through the mutated node gets a shortcut, the arrows touching that node turn around, and any pair of opposite arrows cancels. Here are three nodes in a row. Mutate the middle one: x2 is replaced by (x1 + x3)/x2, and the line becomes a triangle. All the variables you can reach this way generate the cluster algebra.

Three theorems sit at the heart of the subject. First, the Laurent phenomenon, proved by Fomin and Zelevinsky: however long you keep mutating, every variable is a fraction whose bottom is only a product of the starting variables. It explains a puzzle from the 1980s: why the Somos-4 sequence, 1, 1, 1, 1, 2, 3, 7, 23, and on, stays whole. Its twelfth term is 188,807 divided by 23, which is exactly 8,209. Second, positivity: the numbers on top are never negative. Lee and Schiffler proved that for a broad class in 2015, and Gross, Hacking, Keel and Kontsevich more generally in 2018. Third, the finite type classification: the cluster algebras with finitely many variables match the Dynkin diagrams, four families and five exceptions. The largest exception, E8, has 128 variables in 25,080 clusters. All of this is known mathematics.

On November 10, 2026, Axiom Math announced a Lean library for the first seven chapters of the textbook Introduction to Cluster Algebras, by Fomin, Lauren Williams and Zelevinsky. The repository was created a week earlier, with a single commit. By our count it has about 330,000 lines of Lean, more than 90,000 of them certificate data for the type E computations, and our text search finds no sorry and no axiom in the library itself. Axiom’s project site counts 1,429 items from the book: 1,348 formalized, 31 assumed, and 50 excluded. The Laurent phenomenon is in, with Somos-4, and so is the classification, with the E8 counts checked by Lean’s kernel. Positivity is not: the post says it is outside the scope. This is known mathematics, formalized. There is no new theorem.

What it doesn’t claim

The fine print is in the assumptions. Lean checks that a conclusion follows from the hypotheses written into the theorem, nothing more. Here, results the book cites from elsewhere, such as the Cartan–Killing classification from Lie theory, and some exercises the book leaves to the reader, are not proved. They are passed in as hypotheses, so each statement shows what it rests on, and the post says so openly. But they reach far. The Lean version of the Laurent phenomenon takes four of them, including the exercise that mutating twice at the same node changes nothing. So the Somos-4 theorem rests on the same four. The classification takes thirteen hypothesis inputs, with the Cartan–Killing classification first. These are established results, proved on paper; they are just not proved in Lean here.

No new theorem: this is known mathematics, formalized. Positivity (Lee–Schiffler 2015; Gross–Hacking–Keel–Kontsevich 2018) is outside the library’s scope, by Axiom’s own account, and so are the physics applications.

Where it stands

Released by Axiom

Repository created November 3, 2026, with one commit, 39b9ed0 (“Publication of Files”, by Kenny Lau); blog post and project site on November 10. The development history is not public.

Machine checks

One GitHub CI run on the publication commit built the library successfully (an 89-minute job, 9,548 build jobs); it did not run the comparator. A challenge file restates 11 headline statements in a file that imports only Mathlib (with its own definitions written out), and a comparator configuration allows only Lean’s three standard axioms. The README says the comparator accepted the library locally (Lean’s kernel and nanoda); no log is published. The Laurent phenomenon is not one of the 11.

Human review of the Lean

Not described. Axiom’s project site: “AI agents (Anthropic’s Claude) … formalized the blueprint entry by entry”; mathematicians decided the scope, the assumptions and the treatment of exercises. The site’s data label every declaration “reviewed” (rather than “draft, awaiting review”) without saying who reviewed it or how. The blog post lists 32 people and does not mention AI; the README says nothing about authorship.

Independent check

None found as of November 10, 2026: no outside build, review, published comparator log or expert reaction.

Peer reviewed

No (there is no paper).

Lean library, by Axiom

Lean v4.35.0 on Mathlib’s v4.35.0 release (56a0058), Mathlib only (no Stacks or Weil dependency); no sorry and no axiom declarations (our text grep). Cited results and some exercises are assumed as hypotheses: the Laurent phenomenon takes 4, the finite type classification 13. Not built or run by us.

Last checked November 10, 2026. Where it stands. Released: the repository on November 3, the post on November 10. Machine checks: a successful CI build, a comparator file, and a local comparator run that the README reports but does not publish. Human review of the Lean code: not described, beyond a reviewed field in the site’s data. Independent check: we found no outside build, review or expert reaction yet. Peer review: none, as there is no paper. And every Lean theorem holds only under its stated hypotheses. Not built or run by us.

This is outside OpenAI’s math catalogue. It follows AX01, Axiom’s Lean proof of the classification of finite simple groups, AX06, the Stacks Project, and AX07, the Weil conjectures. If it holds, the foundations of cluster algebras are now Lean theorems that others can build on, under the hypotheses they state. Positivity is not formalized in this library; the post lists it as work for the future. See AX07, AX06 and AX01.

The checks

1. Comparator and CI. Here this release goes further than the Weil library in AX07. A challenge file restates eleven headline results, depending only on Mathlib, with its own definitions written out and sorry as each proof. Lean’s comparator tool can then confirm that the library proves exactly those statements, using only Lean’s three standard axioms. The README says the comparator accepted the library locally, with Lean’s kernel and a second checker called nanoda. We found no published log of that run. There is also continuous integration: one GitHub run, on the publication commit, built the library successfully in about an hour and a half. That run did not run the comparator. And the eleven include the classification, with its hypotheses, but not the Laurent phenomenon.
2. Who wrote it? The blog post lists 32 people, with Colin Defant and Alex Sorokin as core contributors and Ken Ono among the others. Like the Weil post, it does not mention AI, and the README says nothing about authorship. Axiom’s project site does: AI agents, Anthropic’s Claude, working with Axiom’s own tooling, formalized the blueprint entry by entry, while mathematicians decided the scope, the assumptions and how exercises were treated. The site’s data put every declaration in a tree labelled reviewed, rather than draft, awaiting review. It does not say who reviewed the Lean code, or how. The three documents describe the same work differently.
3. What it sits on. What it sits on. The library depends on Mathlib alone, at its Lean v4.35.0 release. It does not use Axiom’s Stacks library from AX06, or the Weil library from AX07. About 2,300 tags link Lean declarations to numbered items of the book, so a reader can trace each result back to the text.

The numbers in the video

• Ours: x_(n+1) = (x_n + 1)/x_(n−1) from 1, 1 gives 1, 1, 2, 3, 2, 1, 1 (period 5); with letters, x3 = (x2 + 1)/x1, x4 = (x1 + x2 + 1)/(x1x2), x5 = (x1 + 1)/x2, then x1, x2 again: monomial denominators, positive coefficients (sympy). The library proves the same 5-periodicity (RankTwo/A11.lean).
• Ours: the quiver 1 → 2 → 3 mutated at 2 becomes 1 → 3, 3 → 2, 2 → 1, and x2·x2′ = x1 + x3.
• From Axiom’s post: Somos-4 1, 1, 1, 1, 2, 3, 7, 23, 59, 314, 1529, 8209, with 59·1529 + 314² = 188,807 = 23·8209 (we recomputed); E8: 128 cluster variables and 25,080 clusters (the Lean statement; we rechecked with the classical formulas).
• Ours: the repository at 39b9ed0 has 505 Lean files and 330,722 lines, 92,738 of them type E certificate data, and 2,289 @[cluster_algebras] tags; our text grep finds no sorry, admit, native_decide or axiom declaration in the library (the challenge file has 11 sorry by design).
• Axiom’s project site: 1,429 blueprint items, 1,348 formalized, 31 assumed, 50 excluded; 2,289 Lean declarations.

Read the source

• “Cluster Algebras, Formalized in Lean”, Axiom Math blog post, November 10, 2026.
• AxiomMath/ClusterAlgebras, the Lean repository (Apache 2.0; not built or run by us): its README, challenge file, comparator configuration and assumed results.
• Axiom’s project site (blueprint, dependency graph, mutation playground).
• S. Fomin, L. Williams, A. Zelevinsky, Introduction to Cluster Algebras, Chapters 1–3 (arXiv), and the later chapters linked from the post.

AI Proved What? is independent and not affiliated with Axiom Math, OpenAI, Anthropic, or the book’s authors.

Transcript

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.