Claims

../

2023_02_10_kelley_meka: Theorem 1.1 of Kelley and Meka (FOCS 2023) bounds a progression-free subset of the first N integers by N over any fixed power of log N; accepted on the site's credit and Bloom and Sisask's refereed exposition.

2026_09_23_openai: OpenAI's September 2026 Theorem 1.1 bounds r_k(N) by C_k N exp(-c_k (log N)^(eps_k)) for k >= 3, at k = 3 below N over any power of log N; its Lean proves a weaker bound a library lemma turns into the problem's statement.

---