Status
On this page
Status
Topics
Status
On this page
Status
Topics
Let be infinite sets such that contains all large integers. Let and similarly for . Is it true that if then
as ?
Source: erdosproblems.com/785
An accepted solution exists. The statement is true.
The site labels the problem PROVED (LEAN); the Lean qualifier is explained under Formalization. The status-defining source is the theorem of Sárközy and Szemerédi [SaSz94] (Acta Math. Hungar. 64 (1994), 237--245, refereed): for infinite with containing every large integer and , the excess tends to infinity and is not even . Chen and Fang proved the conclusion under the weaker hypotheses [ChFa10] and then [ChFa14], and sharpened the excess to exceed every power of [ChFa15]; Ruzsa [Ru17] proved with , nearly best possible by his construction. The claim pages are Sárközy and Szemerédi (accepted on the refereed publication and the site's credit), Fang and Chen (2010), Fang and Chen (2014) and Chen and Fang (2015) (each accepted on its refereed publication and the site's credit), Ruzsa (accepted on the refereed publication and the site's credit; the proof van Doorn formalized in Lean in March 2026, a development the corpus has not built), and the 2026 proof claim of van Doorn, Liu and Tang for Chen's conjectured threshold , a generalization of the problem (claimed; the proof claim names GPT-5.6 Sol as the system that wrote the note, and the Lean proof is by Aristotle; no review recorded).