Formalizing the Solution to the Cap Set Problem

Johannes H\"olzl; Robert Y. Lewis; Sander R. Dahmen

arxiv: 1907.01449 · v1 · pith:GTJFGNAFnew · submitted 2019-07-02 · 💻 cs.LO · math.CO

Formalizing the Solution to the Cap Set Problem

Sander R. Dahmen , Johannes H\"olzl , Robert Y. Lewis This is my paper

Pith reviewed 2026-05-25 10:19 UTC · model grok-4.3

classification 💻 cs.LO math.CO

keywords cap set problemformalizationLeanarithmetic progressionfinite fieldupper boundproof assistantpolynomial method

0 comments

The pith

The Ellenberg-Gijswijt upper bound on cap sets has been encoded and verified inside the Lean proof assistant.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper constructs a complete formalization in Lean of the Ellenberg-Gijswijt argument that yields an upper bound on the size of subsets of F_q^n without three-term arithmetic progressions. The formalization reproduces both the general bound and explicit numerical results for the case q=3. A sympathetic reader would care because the work shows that a recent, elementary proof published in the Annals can be rendered into machine-checkable form by following the original steps directly. If the encoding is faithful, the bound is now independently verified without reliance on human inspection of the details.

Core claim

We have built a Lean formalization that faithfully follows the original pen-and-paper argument of Ellenberg and Gijswijt, thereby establishing the same upper bound on the size of subsets of F_q^n with no three-term arithmetic progression and supplying concrete values of the bound for q=3.

What carries the argument

A direct encoding in Lean of the original argument that constructs the bound by mirroring each step of the pen-and-paper reasoning.

If this is right

The Ellenberg-Gijswijt bound holds for all n and q.
Concrete upper bounds for the cap set problem are now machine-verified for small values of n when q=3.
The polynomial-based construction used to obtain the bound can be inspected and reused inside the formal system.
Similar elementary arguments from recent mathematics can be turned into verified formal proofs by the same direct translation approach.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The verified formalization could be extended to compute explicit bounds for additional small values of q or n that the original paper left as exercises.
Once inside Lean, the bound becomes available as a reusable lemma for further formal work on related questions in additive combinatorics.
The same translation method could be applied to other short, clever proofs that rely on polynomial identities over finite fields.

Load-bearing premise

The Lean code accurately captures every inference of the original argument without introducing translation gaps, omitted cases, or incorrect library lemmas.

What would settle it

An explicit counterexample in some small dimension n and q=3 where a set larger than the formally derived bound is exhibited, or an independent audit that finds a logical step in the Lean code missing from the published argument.

read the original abstract

In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of $\mathbb{F}^n_q$ with no three-term arithmetic progression. This problem has received much mathematical attention, particularly in the case $q = 3$, where it is commonly known as the \emph{cap set problem}. Ellenberg and Gijswijt's proof was published in the \emph{Annals of Mathematics} and is noteworthy for its clever use of elementary methods. This paper describes a formalization of this proof in the Lean proof assistant, including both the general result in $\mathbb{F}^n_q$ and concrete values for the case $q = 3$. We faithfully follow the pen and paper argument to construct the bound. Our work shows that (some) modern mathematics is within the range of proof assistants.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Lean formalization of the Ellenberg-Gijswijt cap set proof works and shows proof assistants can handle recent Annals-level combinatorics.

read the letter

This paper gives a Lean formalization of the 2016 Ellenberg-Gijswijt upper bound on cap sets in F_q^n, including the concrete q=3 numbers. They follow the original argument step by step and supply the code in the repository. That is the actual contribution: a machine-checked version of a high-profile combinatorial proof rather than any new bound or technique. The formalization covers both the general case and the specific application, which is solid work given the length and structure of the pen-and-paper version. Soundness rests on Lean’s kernel once the definitions and lemmas are accepted, and there are no obvious circularities or invented parameters. The main soft spot is the usual one for formalizations: whether every inference translates without gaps or library mismatches. The authors address this by releasing the full development, so readers can check directly. Minor additional point is that the paper stays tightly focused on verification and does not explore broader implications or extensions. This is useful for the formal-methods community and for anyone tracking what kinds of modern math can now be verified. It is not a new mathematical result, so its audience is narrower than the original Annals paper, but the verification itself is non-trivial. I would send it to peer review; the central claim is concrete and checkable, and the repository makes the work reproducible.

Referee Report

0 major / 2 minor

Summary. The manuscript presents a formalization in the Lean proof assistant of the 2016 Ellenberg-Gijswijt proof, which gives a new upper bound on the size of subsets of F_q^n without three-term arithmetic progressions; the work covers both the general case and the concrete cap-set bound for q=3, claiming to follow the original pen-and-paper argument faithfully and thereby demonstrating that certain modern combinatorial proofs lie within the scope of current proof assistants.

Significance. If the formalization is faithful, the result supplies machine-checked confirmation of a high-profile Annals of Mathematics theorem, supplies a reusable Lean library for related combinatorial arguments, and provides concrete evidence that proof assistants can now handle the length and conceptual depth of recent research-level mathematics.

minor comments (2)

[Section 1] Section 1: the statement that the formalization 'faithfully follows' the original argument would be strengthened by an explicit list (perhaps in an appendix) of the main lemmas and their Lean counterparts.
[Abstract and §1] The repository URL in the abstract and introduction should be accompanied by a permanent archive identifier (e.g., Zenodo DOI) to guarantee long-term reproducibility.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary, significance assessment, and recommendation to accept the manuscript. There are no major comments requiring a point-by-point response.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper is a formalization in Lean of the independent 2016 Ellenberg-Gijswijt proof (published in Annals of Mathematics by different authors). Its derivation chain consists of faithfully encoding that external argument; no load-bearing steps reduce by construction to self-citations, fitted parameters renamed as predictions, or self-definitional relations within this work. The cited result is externally verifiable and not dependent on the present authors' prior claims.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The formalization encodes the existing Ellenberg-Gijswijt argument; it introduces no new free parameters, ad-hoc axioms, or invented entities beyond the standard mathematical foundations already present in Lean’s mathlib.

axioms (1)

standard math Standard axioms of mathematics as encoded in Lean’s mathlib (dependent type theory with classical logic and choice)
Invoked throughout the formalization to justify the steps of the original proof.

pith-pipeline@v0.9.0 · 5676 in / 1169 out tokens · 30691 ms · 2026-05-25T10:19:03.570005+00:00 · methodology

Formalizing the Solution to the Cap Set Problem

Core claim

What carries the argument

If this is right

Where Pith is reading between the lines

Load-bearing premise

What would settle it

discussion (0)