Motivation

Erdős asked, repeatedly and with a rising price tag, for an asymptotic formula for the largest subset of $\{1,\dots,N\}$ that contains no arithmetic progression of a given length. He offered 1000 dollars for it in [Er97c] and 10000 dollars in [Er81, p.4], where he called the question "probably enormously difficult"; elsewhere he described it as "probably unattackable at present". Most of modern additive combinatorics — the density increment method, the triangle removal lemma, Gowers uniformity norms, the arithmetic regularity lemma — grew out of attempts on this single question, and the answer is still unknown, even in the first non-trivial case $k=3$.

Timeline.

• 1936: Erdős and Turán conjecture that $r_k(N)=o(N)$ for every $k$.
• 1946: Behrend constructs large progression-free sets, giving $r_3(N)\ge N\exp(-c\sqrt{\log N})$.
• 1953: Roth proves $r_3(N)=o(N)$, with the quantitative form $r_3(N)\ll N/\log\log N$.
• 1961: Rankin generalises Behrend, giving $r_k(N)\ge N\exp(-c_k(\log N)^{1/(k-1)})$.
• 1969, 1975: Szemerédi proves $r_4(N)=o(N)$ and then $r_k(N)=o(N)$ for all $k$, settling Erdős–Turán.
• 1977: Furstenberg reproves Szemerédi's theorem ergodically, with no effective bound.
• 1998, 2001: Gowers introduces uniformity norms and obtains $r_k(N)\ll N(\log\log N)^{-c_k}$, the first effective bound for general $k$.
• 2017: Green and Tao obtain $r_4(N)\ll N(\log N)^{-c}$.
• 2020: Bloom and Sisask obtain $r_3(N)\ll N(\log N)^{-1-c}$, the first bound past the $N/\log N$ barrier.
• 2023: Kelley and Meka obtain $r_3(N)\le N\exp(-c(\log N)^{1/12})$.
• 2024: Leng, Sah and Sawhney obtain $r_k(N)\ll N\exp(-(\log\log N)^{c_k})$ for $k\ge5$.

Every upper bound in this list is still astronomically far from Behrend's lower bound, and no candidate asymptotic formula has been proposed for any $k\ge3$.

Setting

Fix an integer $k$. A non-trivial $k$-term arithmetic progression is a list $a,\,a+d,\,a+2d,\dots,a+(k-1)d$ of natural numbers with common difference $d>0$; the requirement $d>0$ is what "non-trivial" means, and it forces the $k$ terms to be distinct. A finite set $A\subseteq\mathbb N$ is $k$-AP-free if it contains no such progression. Write

$$r_k(N)\;=\;\max\bigl\{\,|A| \;:\; A\subseteq\{1,\dots,N\},\ A\ \text{is}\ k\text{-AP-free}\,\bigr\}.$$

The mission takes its formal definition of $r_k$ verbatim from the formal-conjectures entry for this problem, so that the goal below is literally the statement recorded there. In that development a set is called free of progressions of length $l$ when every subset of it that is an arithmetic progression of length $l$ forces $l\le1$. Progressions of length $0$ and $1$ count as trivial, so under that convention every set is free of them and $r_0(N)=r_1(N)=N$; the interesting range begins at $k\ge2$. Every statement in this mission that depends on the convention carries an explicit hypothesis on $k$.

On that range, $r_k(N)$ is non-decreasing in both $N$ and $k$, satisfies $r_k(M+N)\le r_k(M)+r_k(N)$, and hence, by Fekete's subadditivity lemma, $r_k(N)/N$ converges. Szemerédi's theorem is the statement that the limit is $0$; the whole difficulty of this mission lies in how fast it goes to $0$.

Formalization targets

Goal

$$r_k(N)\;=\;o_k\!\left(\frac{N}{\log N}\right)\qquad\text{for every }k>1 .$$

This is erdos_142.variants.lower of the formal-conjectures file for Erdős 142, reproduced binder for binder, over that file's own definition of $r_k$.

The headline theorem in that file, erdos_142, states $r_k(N)=\Theta(f)$ with the comparison function left as an answer(sorry) placeholder, and the same is true of its variants.upper and variants.three. Those are not closed propositions and cannot serve as a mission goal: the literal request of Erdős Problem #142 — "prove an asymptotic formula for $r_k(N)$" — has no known right-hand side for any $k\ge3$, which is exactly why the file leaves a hole there. variants.lower is the one formalizable target in the file, and it is also the strongest precisely-stated form the problem page attaches to #142: Erdős offered 5000 dollars for (essentially) exactly it, as recorded under Erdős Problem #3. It is known for $k=3$ — it follows from Bloom–Sisask 2020, and a fortiori from Kelley–Meka 2023 — trivial for $k=2$, where $r_2(N)=1$, and open for every $k\ge4$. It fixes no constants, so no future improvement can invalidate it.

A weaker open question

$$\frac{r_k(n)}{r_{k+1}(n)}\longrightarrow 0\qquad\text{for some }k\ge3 .$$

Erdős remarked in [Er80, p.92] that even this separation between consecutive progression lengths is not known. Here [Er80] is the erdosproblems.com bibliography key for Erdős's 1980 paper; it is a citation, not a pointer to Erdős Problem #80, which is an unrelated question about books in graphs. This statement has no counterpart in formal-conjectures: the file for #142 contains only the $\Theta$, $o$ and $O$ variants above, and the only two files in that repository that mention $r_k$ at all are the ones for #142 and #139.

Significance

Proving $r_k(N)=o_k(N/\log N)$ for all $k$ yields, by a standard summation argument, Erdős's conjecture that every $A\subseteq\mathbb N$ with $\sum_{a\in A}1/a=\infty$ contains arbitrarily long arithmetic progressions — the 5000-dollar Erdős Problem #3, of which the Green–Tao theorem on primes is the best-known special case. Below that threshold, quantitative bounds on $r_k$ control the density at which progressions must appear in any concrete set, and are the input to results on progressions in the primes, in sumsets, and in sparse random subsets of the integers.

Formalization status is uneven, and this mission is designed around that gap. Mathlib already contains the $k=3$ theory in a usable form: the predicate ThreeAPFree, the Roth number rothNumberNat, its subadditivity, and a complete formalization of Behrend's construction (Behrend.roth_lower_bound). Mathlib does not contain Roth's theorem, Szemerédi's theorem, or any of the modern upper bounds; to the best of current knowledge none of Roth, Szemerédi, Gowers, Green–Tao, Kelley–Meka or Leng–Sah–Sawhney has a machine-checked proof anywhere. The formal-conjectures entry states the problem but proves nothing: every declaration in it is a sorry. Two of this mission's targets are taken from that repository — the goal from its file for #142, and the Szemerédi milestone from its file for #139, which uses the same $r_k$; those are the only two files there that mention $r_k$. The milestones therefore split cleanly: the first six are reachable now on top of Mathlib, and the last five are open formalization projects of independent value.

Difficulty

Every known upper bound for $r_k$ runs a density increment: if $A\subseteq\{1,\dots,N\}$ of density $\delta$ has no $k$-term progression, find a long subprogression on which $A$ has density $\delta(1+c(\delta))$, and iterate. The bound this produces is governed entirely by two quantities — how large the increment $c(\delta)$ is, and how much of the interval survives one step. For $k\ge4$ the increment is extracted from an inverse theorem for the Gowers $U^{k-1}$-norm, and the best available correlation bounds there are quasipolynomial in $\delta$; iterating a quasipolynomial increment cannot do better than $N\exp(-(\log\log N)^{c})$, which is nowhere near $N/\log N$. Reaching $N/\log N$ requires an increment with polynomial dependence on $\delta$ together with a subprogression of polynomial length, and that combination is currently available only for $k=3$, through the sifting and almost-periodicity machinery of Kelley–Meka. No soft or averaging argument can substitute: Behrend's construction shows the truth at $k=3$ is $N\exp(-\Theta(\sqrt{\log N}))$, so the answer is not a power of $\log N$ and cannot be produced by any argument whose output has that shape.

Formalization scope

The mission's definition file Erdos142Basic carries two layers, and every statement in the mission is written against them.

1. The source definitions, ported verbatim. IsAPOfLengthWith, IsAPOfLength, IsAPOfLengthFree and r are the declarations of the formal-conjectures entry, transcribed unchanged into the mission's namespace: a set is an arithmetic progression of length $l$ with first term $a$ and difference $d$ when it has exactly $l$ elements and equals $\{a+nd : n<l\}$; it is free of length-$l$ progressions when every progression of length $l$ inside it forces $l\le1$; and $r_k(N)$ is the supremum of $|S|$ over subsets $S\subseteq\{1,\dots,N\}$ free of length-$k$ progressions. The ground set is Finset.Icc 1 N, and the supremum is sSup over $\mathbb N$; the file proves the two facts that make it a genuine maximum (le_r and r_le).

2. An elementary handle. HasAP k A is ∃ a d, 0 < d ∧ ∀ i < k, a + i * d ∈ A, and APFree k A its negation. This form carries no cardinality side condition in $\mathbb N\cup\{\infty\}$ and is what a solver actually wants to induct on. The first milestone is exactly the bridge between the two layers.

Two consequences of the source convention are worth stating plainly, because the prose is silent about them. Length-$0$ and length-$1$ progressions are trivial, so every set is free of them and $r_0(N)=r_1(N)=N$; monotonicity of $r_k$ in $k$ therefore holds only from $k\ge2$ onward, and the corresponding milestone carries that hypothesis. Asymptotic statements use Asymptotics.IsLittleO and Filter.atTop over $\mathbb N$ with real-valued casts, and real division is Lean's, so (N : ℝ) / Real.log N is $0$ at $N=1$; this is invisible to atTop.

A trivializing formalization is ruled out by construction: one milestone asserts $r_3(N)=$ rothNumberNat N, pinning this development against Mathlib's independently written definition of the Roth number, so a vacuous or mis-quantified notion of progression-freeness cannot survive. That milestone, the bridge milestone above it, and the monotonicity milestone have all been checked to be provable before this proposal was drafted.

A full development needs: discrete Fourier analysis on $\mathbb Z/N\mathbb Z$, Bohr sets and their regularity, the arithmetic regularity lemma, Gowers uniformity norms and the inverse theorem for them, and — for the lower bounds — sphere-counting in high-dimensional boxes (already in Mathlib via Behrend). All of this is reusable well beyond this mission. Contributions of any kind are welcome, including partial results: quantitative bounds weaker than the cited ones, the $k=3$ case of a general-$k$ milestone, and reusable Fourier-analytic infrastructure are all valuable even when they do not close a milestone.

Selected references

• Erdős Problem #142. https://www.erdosproblems.com/142
• Erdős Problem #3. https://www.erdosproblems.com/3
• Erdős Problem #139 (Szemerédi's theorem in the $r_k$ formulation), linked from #142. https://www.erdosproblems.com/139
• Google DeepMind, formal-conjectures, FormalConjectures/ErdosProblems/142.lean — the source of the goal statement and of the definition of $r_k$. https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/142.lean
• F. A. Behrend, On sets of integers which contain no three terms in arithmetical progression, Proc. Nat. Acad. Sci. USA 32 (1946), 331–332. https://doi.org/10.1073/pnas.32.12.331
• K. F. Roth, On certain sets of integers, J. London Math. Soc. 28 (1953), 104–109. https://doi.org/10.1112/jlms/s1-28.1.104
• R. A. Rankin, Sets of integers containing not more than a given number of terms in arithmetical progression, Proc. Roy. Soc. Edinburgh Sect. A 65 (1961), 332–344.
• E. Szemerédi, On sets of integers containing no $k$ elements in arithmetic progression, Acta Arith. 27 (1975), 199–245. https://doi.org/10.4064/aa-27-1-199-245
• W. T. Gowers, A new proof of Szemerédi's theorem, Geom. Funct. Anal. 11 (2001), 465–588. https://doi.org/10.1007/s00039-001-0332-9
• B. Green and T. Tao, New bounds for Szemerédi's theorem, III: A polylogarithmic bound for $r_4(N)$, Mathematika 63 (2017), 944–1040. https://arxiv.org/abs/1705.01703
• T. F. Bloom and O. Sisask, Breaking the logarithmic barrier in Roth's theorem on arithmetic progressions, arXiv:2007.03528. https://arxiv.org/abs/2007.03528
• Z. Kelley and R. Meka, Strong bounds for 3-progressions, arXiv:2302.05537. https://arxiv.org/abs/2302.05537
• J. Leng, A. Sah and M. Sawhney, Improved bounds for Szemerédi's theorem, arXiv:2402.17995. https://arxiv.org/abs/2402.17995