Motivation

Which sets of positive integers are forced to contain long arithmetic progressions? Van der Waerden (1927) showed that in any finite colouring of $\mathbb N$ some colour class does; Erdős and Turán (1936) asked for a density version, which became Szemerédi's theorem. Erdős then proposed the strongest natural size condition: divergence of the reciprocal sum. Erdős Problem #3 (erdosproblems.com/3) asks whether every $A\subseteq\mathbb N$ with $\sum_{n\in A}1/n=\infty$ contains arbitrarily long arithmetic progressions. Erdős attached one of his largest prizes to it. The primes are the motivating example: $\sum_p 1/p=\infty$, so a positive answer would contain the Green–Tao theorem.

Timeline.

• 1936 — Erdős and Turán conjecture that sets of positive density contain arbitrarily long progressions.
• 1953 — Roth proves the case $k=3$ of the density conjecture by Fourier analysis.
• 1975 — Szemerédi proves the density conjecture for all $k$.
• 2001 — Gowers gives the first quantitative bounds for all $k$: $r_k(N)\ll N/(\log\log N)^{c_k}$.
• 2008 — Green and Tao prove that the primes contain arbitrarily long progressions.
• 2020 — Bloom and Sisask prove $r_3(N)\ll N/(\log N)^{1+c}$, which settles the case $k=3$ of Erdős Problem #3.
• 2023 — Kelley and Meka prove $r_3(N)\le N\exp(-c(\log N)^{1/12})$.
• 2024 — Leng, Sah and Sawhney prove $r_k(N)\le N\exp(-(\log\log N)^{c_k})$ for every $k\ge5$.

The problem is open for every $k\ge4$.

Setting

A set $S\subseteq\mathbb N$ is an arithmetic progression of length $k$ if $|S|=k$ and $S=\{a,a+d,\dots,a+(k-1)d\}$ for some $a,d\in\mathbb N$ (for $k\ge2$ the size condition forces $d>0$). For $k,N\in\mathbb N$, $r_k(N)$ denotes the largest size of a subset of $\{1,\dots,N\}$ containing no arithmetic progression of length $k$. A set $A$ has divergent reciprocal sum if $\sum_{n\in A}1/n=\infty$.

Formalization targets

Goal (Erdős Problem #3)

For every $A\subseteq\mathbb N$,

$$\sum_{n\in A}\frac1n=\infty\ \Longrightarrow\ A\ \text{contains arithmetic progressions of arbitrarily large length}.$$

This is the formal-conjectures statement erdos_3 with its answer(sorry) instantiated to the conjectured answer yes. A disproof of the goal on the platform settles the problem negatively.

Milestones

• Szemerédi's theorem for sets of positive upper density (the density case), and the existing platform statement $r_k(N)=o(N)$.
• The Green–Tao theorem (the case $A=$ primes).
• The Bloom–Sisask bound on $r_3(N)$ and its corollary, the case $k=3$ of the goal; the Kelley–Meka bound (existing platform statement).
• The Leng–Sah–Sawhney bound for $k\ge5$.
• The partial-summation reduction: bounds $r_k(N)\le N/(\log N)^{1+c_k}$ for all $k\ge3$ imply the goal.

Significance

A positive answer would be a common strengthening of Szemerédi's theorem and the Green–Tao theorem, obtained from a single size condition with no arithmetic structure. Through the reduction milestone, it is closely tied to the quantitative theory of $r_k(N)$: bounds of the shape $N/(\log N)^{1+c}$ for every $k$ would suffice. Formalizing the milestones would also give reusable Lean statements of Szemerédi-type theorems in a common language.

Difficulty

Divergence of $\sum 1/n$ is a very weak condition: such sets can have density zero, and the natural approach through $r_k(N)$ requires bounds just past $N/\log N$. For $k=3$ this barrier was only broken in 2020. For $k\ge4$ the best known bounds (Leng–Sah–Sawhney) save only a power of $\log\log N$ in the exponent, far from what is needed. The Green–Tao method uses pseudorandom majorants specific to the primes and does not apply to arbitrary sets.

Formalization scope

All statements import the published definition file Erdos142Basic, which reproduces the formal-conjectures definitions IsAPOfLengthWith, IsAPOfLength and the counting function r k N (over $\{1,\dots,N\}$). The reciprocal-sum hypothesis is ¬ Summable (fun a : A ↦ 1 / (a : ℝ)); the element $0$, if present, contributes $1/0=0$. "Arbitrarily long" is written as ∃ᶠ k in atTop, which is equivalent to "every length" because sub-progressions of progressions are progressions. Bounds stated in the literature with $\ll$ are written without a multiplicative constant and with "for all sufficiently large $N$"; the constant can be absorbed into the exponent. Contributions formalizing partial summation over sets of naturals and the equivalence of the "frequently" and "for every $k$" forms are welcome.

Selected references

• P. Erdős and P. Turán, On some sequences of integers, J. London Math. Soc. 11 (1936).
• K. F. Roth, On certain sets of integers, J. London Math. Soc. 28 (1953).
• E. Szemerédi, On sets of integers containing no k elements in arithmetic progression, Acta Arith. 27 (1975).
• W. T. Gowers, A new proof of Szemerédi's theorem, Geom. Funct. Anal. 11 (2001).
• B. Green and T. Tao, The primes contain arbitrarily long arithmetic progressions, Ann. of Math. 167 (2008).
• T. F. Bloom and O. Sisask, Breaking the logarithmic barrier in Roth's theorem on arithmetic progressions, arXiv:2007.03528 (2020).
• Z. Kelley and R. Meka, Strong bounds for 3-progressions, FOCS 2023, arXiv:2302.05537.
• J. Leng, A. Sah and M. Sawhney, Improved bounds for Szemerédi's theorem, arXiv:2402.17995 (2024).
• T. F. Bloom, Erdős Problem #3, https://www.erdosproblems.com/3