The polynomial Freiman-Ruzsa conjecture

The polynomial Freiman–Ruzsa conjecture, also called Marton's conjecture, is a statement in additive combinatorics about sets that are nearly closed under addition. In November 2023 W. T. Gowers, Ben Green, Freddie Manners and Terence Tao proved it in characteristic 2, and in about three weeks a group of volunteers led by Tao checked the proof in Lean. This page describes the result, how the checking was organised, and what it found.

The statement

Take the strings of $n$ bits, added place by place with 1 + 1 = 0; mathematicians write this space ${𝔽}_2^n$. For a set $A$ of such strings, $A+A$ is the set of all sums of two of its elements. If $A$ is a subspace, adding gives nothing new and $A+A=A$. The conjecture says the converse holds in a robust form: if $A+A$ is not much larger than $A$, then $A$ is close to a subspace.

In the form Tao gave on his blog: if $|A+A|\le K|A|$, then $A$ can be covered by at most $2K^{12}$ translates of a subspace $H$ with $|H|\le |A|$. What matters is that the number of translates is bounded by a power of $K$; the best earlier bound, which Tao attributes to Konyagin, grew faster than any power. The conjecture connects a simple test on sums with algebraic structure, and it has links to areas such as coding theory and cryptography; Quanta Magazine reported that Gil Kalai had called it "a holy grail" of the field.

The proof

The paper "On a conjecture of Marton" was posted on 9 November 2023 and revised on 12 December 2023. Its argument works with the entropy of random variables, in Shannon's sense, rather than with Fourier analysis, and it proceeds by induction on a doubling constant defined through entropy. It was published in the Annals of Mathematics in 2025. In April 2024 the same four authors extended the method to abelian groups of bounded torsion.

The formalisation

In his blog post of 13 November 2023 Tao wrote that he planned to formalise the paper in Lean 4. The project was started by Tao, Yaël Dillies and Bhavik Mehta, and less than a week after its launch a significant part of the paper was already formalised in full or in part. About 25 volunteers took part.

The work was organised with Blueprint, a tool written by Patrick Massot. A blueprint is a human-readable LaTeX version of the proof in which each definition and lemma is linked to its Lean counterpart. From it the tool draws a dependency graph: lemmas appear as bubbles and definitions as rectangles, and the colours show progress. Green means fully formalised; blue means the statement is formalised and its proof is ready to be formalised. When a proof compiles, its author marks it done in the LaTeX by hand, since the tool does not check that mark itself. Tasks were handed out on the Lean community's chat forum: Tao posted threads of outstanding tasks, contributors claimed them first come, first served, and he kept the list up to date by hand.

On 5 December 2023 Tao announced that the project had succeeded after three weeks: every node of the dependency graph was green, and Lean reported that the conjecture follows from the standard axioms. The formalisation found a few minor typos in the paper.

The final statement, as it stands in the project's Lean files, uses the Mathlib library and is shown here without its proof:

theorem PFR_conjecture {G : Type*} [AddCommGroup G] [Module (ZMod 2) G]
    {A : Set G} {K : ℝ} (hA₀ : A.Nonempty) (Afin : A.Finite)
    (hA : (A + A).ncard ≤ K * A.ncard) :
    ∃ (H : Submodule (ZMod 2) G) (c : Set G), c.Finite ∧ (H : Set G).Finite ∧
      Nat.card c < 2 * K ^ 12 ∧ (H : Set G).ncard ≤ A.ncard ∧ A ⊆ c + H := by
  -- the proof follows in the project's files

Read in words: G is any space of the kind described above, a vector space over the two-element field; A is a finite, nonempty set in it whose sum set has at most K times as many elements; then there are a subspace H, no larger than A, and a finite set c of fewer than $2K^{12}$ shifts, such that A lies inside c + H. Every hypothesis is written out. The hypothesis that A is nonempty is one example: it was added to the Lean statement before it appeared in the blueprint's LaTeX.

After the main result

When the main goal was reached, a second stage formalised several consequences of the theorem and an argument of Jyun-Jie Liao that lowers the exponent from 12 to 11; the project page records that stage as complete, and names among the theorems its Lean files prove both the extension to groups of bounded torsion and a further refinement of Liao's that lowers the exponent to 9.

What it showed

The blueprint divided a paper of some 35 journal pages into small nodes, each of which a contributor could take on without mastering the whole argument, while Lean checked that the pieces fitted together. In that arrangement the organisers did not need to trust a contribution, only Lean's verdict on it. The equational theories project cites this project as its precedent and automated the claiming of tasks that had been done by hand here.

The formalisation did not change the mathematics; the errors it found were minor typos. What it changed was the evidence: a reader who doubts the theorem can check the Lean proof instead of the paper.

Next

• The Fermat's Last Theorem project, a far larger formalisation organised the same way.
• Research mathematics, for other formalised results.