Smallest $k$: 2-colour the plane with no red unit pair and no blue unit-spaced $k$-AP (Erdős #188)
Statement
What is the smallest $k$ for which the plane $\mathbb{R}^2$ admits a red/blue colouring such that (i) no two red points are at distance exactly $1$, and (ii) there is no $k$-term arithmetic progression of blue points whose consecutive gaps have length $1$ — that is, no $k$ collinear blue points $p, p+v, p+2v, \ldots, p+(k-1)v$ with $\lvert v\rvert = 1$? Equivalently, determine the least $k$ for which such a colouring is possible.
Acceptance. FULLY RESOLVES: determine the exact value of $k$ with proof — both a construction (an explicit red/blue colouring of $\mathbb{R}^2$ realizing the value, with a verification that it has no red unit-distance pair and no blue $k$-term unit-spaced AP) and a matching lower bound (a proof that the value $k-1$ is impossible). ADVANCES: (a) improve the lower bound beyond the best stated in the background (currently $k\geq 6$) by exhibiting a finite planar configuration on which every red-unit-free $2$-colouring contains a blue unit-spaced arithmetic progression of the required length, with a machine-checkable (e.g. SAT/DRAT) certificate; (b) establish the first rigorous finite upper bound on $k$ via an explicit colouring construction with a verifiable argument. Deliver the finite-configuration certificate with solver logs, or the explicit colouring plus verification.
Background
Asked by Erdős and Graham [ErGr79], [ErGr80]. Known bounds: Erdős, Graham, Montgomery, Rothschild, Spencer, and Straus [EGMRSS75] proved $k\geq 5$, and Tsaturian [Ts17] improved this to $k\geq 6$. Erdős and Graham claimed $k\leq 10{,}000{,}000$ ('more or less') but gave no proof, so no rigorous upper bound is on record. Historical subtlety: Erdős and Graham originally allowed any $k$-term blue arithmetic progression (arbitrary common difference), but Alon observed that then no finite $k$ works — along a line, either two red points lie at distance $1$, or the blue set together with its shift by $1$ covers all integers, forcing arbitrarily long blue progressions by van der Waerden's theorem; hence the intended (and here stated) restriction to unit common difference. A Lean formalisation exists in the google-deepmind/formal-conjectures repository (188.lean). No cash prize is attached. Listed as open on erdosproblems.com/188 (fetched 2026-07-13, status 'open', tagged 'geometry | ramsey theory'). The attacker's tool: the lower bound is a finite-configuration question amenable to SAT/ILP — exhibit a finite planar point set on which every red-unit-free $2$-colouring forces a blue unit-spaced progression of the target length — while any rigorous upper bound requires an explicit constructive colouring of the plane.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #188 (T. F. Bloom) | website |
| REF-02 | Lean formalisation — google-deepmind/formal-conjectures (Erdős #188) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.