Erdős Problem #1090
PROVED LEANdatabase updated 2026-02-27
The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
Let \(k\geq 3\). Does there exist a finite set \(A\subset \mathbb{R}^2\) such that, in any \(2\)-colouring of \(A\), there exists a line which contains at least \(k\) points from \(A\), and all the points of \(A\) on the line have the same colour? Erdős [Er75f] says Graham and Selfridge proved the answer is yes when \(k=3\). Hunter has observed that, for sufficiently large \(n\), a generic projection of \([k]^n\) into \(\mathbb{R}^2\) has this property, by the Hales-Jewett theorem.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved. The authoritative wording is on erdosproblems.com/1090.Prizenone
Topicsgeometry, ramsey theory
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/1090
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.