PROVED (LEAN): Szemerédi's 1975 theorem, refereed in Acta Arithmetica, answers the question; see the claim page (Szemerédi, 1975). 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 (OpenAI, 2026) 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.