Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated Oct 8

Problem 139

claims/: The 6 claim pages of Problem 139, one per claimant's result; the problem's standing derives from them.

Statement. Let $r_k(N)$ be the size of the largest subset of $\{1,\ldots,N\}$ which does not contain a non-trivial $k$ -term arithmetic progression. Prove that $r_k(N)=o(N)$ .

Status. PROVED (LEAN): Szemerédi's 1975 theorem, refereed in Acta Arithmetica, answers the question; see the claim page. The site's Lean qualification refers to a Lean proof of the theorem in Boris Alexeev's lean-proofs repository, which formal-conjectures points to; the development declares itself a formalization of Szemerédi's theorem and is linked from his claim page, neither built nor audited by this corpus. The OpenAI release's quasipolynomial bound for every fixed $k\ge3$ is a second route, accepted on its claim page through its Lean declaration of a weaker saving that still gives $r_k(N)=o(N)$ , which this corpus's verification built and axiom-checked; no comparator challenge pins that declaration, and the manuscript's own bound is unreviewed. The bounds the site's commentary credits as the best known, Kelley and Meka's for $k=3$ (sharpened by Bloom and Sisask), Green and Tao's for $k=4$ and Leng, Sah and Sawhney's for $k\ge5$ , each prove their instances of the statement with a rate, and each has a partial claim page: Kelley and Meka, Bloom and Sisask, Green and Tao and Leng, Sah and Sawhney.

Source. erdosproblems.com/139, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #139, https://www.erdosproblems.com/139.

References.

[BlSi23] T. F. Bloom and O. Sisask, An improvement to the Kelley-Meka bounds on three-term arithmetic progressions. arXiv:2309.02353 (2023).
[Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115.
[GrTa17] Green, Ben and Tao, Terence, New bounds for Szemerédi's theorem, III: a polylogarithmic bound for $r_4(N)$ . Mathematika (2017), 944-1040.
[KeMe23] Kelley, Z. and Meka, R., Strong Bounds for 3-Progressions. arXiv:2302.05537 (2023).
[LSS24] Leng, J., Sah, A. and Sawhney, M., Improved bounds for Szemerédi's theorem. arXiv:2402.17995 (2024).
[Sz75] Szemerédi, E., On sets of integers containing no $k$ elements in arithmetic progression. Acta Arith. (1975), 199-245.

Formalization. Statement in formal-conjectures, whose entry at its commit of 2026-10-06, linked, carries the category research solved and a formal_proof attribute pointing to the plby/lean-proofs development at a pinned commit; that development was neither built nor audited by this corpus and is linked as a self-declared formalization from Szemerédi's claim page. The OpenAI release's Lean tree proves a weaker quantitative bound that still gives $r_k(N)=o(N)$ , OAI.Erdos3.manuscriptQuantitativeDensityTheorem, which this corpus's verification built at the pinned revision with the toolchain leanprover/lean4:v4.34.1 and found to use only propext, Classical.choice and Quot.sound; no comparator challenge pins it, and its statement was audited against the problem, so it gives formalized evidence on its claim page.

Progress

Not yet compiled.

Known Results

Not yet compiled.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

Linked from (21)

Graph