Claims

../

1975_01_01_szemeredi: Szemerédi's 1975 theorem in Acta Arithmetica that r_k(N) = o(N) for every k, accepted on the refereed publication and the site's credit, with the unaudited Lean formalization of it in Boris Alexeev's repository linked.

2017_05_04_green_tao: Theorem 1.1 of Green and Tao (Mathematika 2017) bounds a subset of the first N integers with no four-term progression by N over a power of log N, which proves the k = 4 instance of Problem 139 with a rate; accepted as refereed.

2023_02_10_kelley_meka: Theorem 1.1 of Kelley and Meka (FOCS 2023) bounds a subset of the first N integers with no three-term progression by N times 2 to the minus a power of log N, the k = 3 instance of Problem 139 with a rate; accepted as reviewed.

2023_09_05_bloom_sisask: Theorem 1 of Bloom and Sisask's 2023 note bounds a subset of the first N integers with no three-term progression by exp(-c (log N)^(1/9)) N, the k = 3 instance of Problem 139 with a sharper rate; a preprint, so claimed.

2024_02_28_leng_sah_sawhney: Theorem 1.1 of Leng, Sah and Sawhney (2024) bounds a subset of the first N integers with no k-term progression by N exp(-(log log N)^(c_k)) for every k at least 5, those instances of Problem 139 with a rate; a preprint, claimed.

2026_09_23_openai: The OpenAI release's bound r_k(N) <= C_k N exp(-c_k (log N)^(eps_k)) for each fixed k at least 3, which gives r_k(N) = o(N) at once; accepted as a second route on a built Lean declaration of a weaker saving that suffices.

---