Problem 140

Let $r_3(N)$ be the size of the largest subset of $\{1,\ldots,N\}$ which does not contain a non-trivial $3$ -term arithmetic progression. Prove that $r_3(N)\ll N/(\log N)^C$ for every $C>0$ .

Source: erdosproblems.com/140

Additive combinatorics
Arithmetic progressions

Wiki page

Status

SolvedProved

An accepted solution exists. The statement is true.

PROVED (LEAN). The site credits the proof to Kelley and Meka [KeMe23], whose Theorem 1.1 gives $r_3(N)\le N\,2^{-c(\log N)^{\beta}}$ for an absolute $\beta>0$ , below $N/(\log N)^C$ for every $C$ ; the claim page Kelley and Meka is accepted on the site's credit and Bloom and Sisask's refereed exposition of the proof (the FOCS 2023 proceedings are not a journal, so the page lists no refereed evidence), and the frontmatter standing derives from it. A second route, the September 2026 release preprint of OpenAI with a Lean library two of whose declarations combine to prove the problem at $k=3$ , is accepted on its claim page (OpenAI, 2026) on those declarations, which this corpus's verification built and axiom-checked; no comparator challenge pins them, and the preprint itself is unreviewed. The site's commentary adds that [ErGr80] and [Er81] conjecture the same bound for every $k$ . No result before the release proves it for any $k\ge4$ , and the release's theorem claims it; the same two Lean declarations give it at each $k\ge4$ by the same combination, as its claim page records. The (Lean) suffix of the site's label traces to the community database's formal-status mark and to the Lean development in Boris Alexeev's lean-proofs repository that declares itself a formalization of Kelley and Meka's result, linked on their claim page and explained under Formalization; this corpus has not built or audited it.

Er81: Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica (1981), 25-42.
Er97c: Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I, Algorithms Combin. 13, Springer (1997), 47--67; printed pp. 50--51: "I offer $500 for a proof that $r_3(n)<n/(\log n)^c$ for every $c$ , and $1000 for any asymptotic formula for $r_k(n)$ ", with $r_k(n)$ defined as the smallest size forcing a $k$ -term progression. Library home: Erdős 1997; paged at Erdős 1997, Problem (p. 51).
ErGr80: Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
KeMe23: Kelley, Z. and Meka, R., Strong Bounds for 3-Progressions. arXiv:2302.05537 (2023); Proceedings of the 2023 IEEE 64th Annual Symposium on Foundations of Computer Science (FOCS 2023), 933--973, doi:10.1109/FOCS57990.2023.00059. Library home: Kelley and Meka 2023.
BlSi23: Bloom, T. F. and Sisask, O., An improvement to the Kelley-Meka bounds on three-term arithmetic progressions. arXiv:2309.02353 (2023). Library home: Bloom and Sisask 2023.
BlSi23a: Bloom, T. F. and Sisask, O., The Kelley--Meka bounds for sets free of three-term arithmetic progressions. Essential Number Theory 2 (2023), no. 1, 15--44, doi:10.2140/ent.2023.2.15; arXiv:2302.07211 (14 February 2023). A refereed exposition of the proof; not held. The site's bibliography does not cite it; its key [BlSi23] is the arXiv preprint above.
OAI26: OpenAI, Quasipolynomial Bounds for Arithmetic Progressions. OpenAI Math Release preprint, 23 September 2026 (family 159, with a Lean library); see the claim page (OpenAI, 2026). Library home: OpenAI 2026.

Problem 140

Status

Proof claims

Discussion