Erdős Problem 645

Reference: erdosproblems.com/645

theorem Erdos645.erdos_645 (c : ℕ → Bool) : ∃ (x : ℕ) (d : ℕ), 0 < x ∧ x < d ∧ ∃ (C : Bool), c x = C ∧ c (x + d) = C ∧ c (x + 2 * d) = C

If ℕ is $2$-coloured then there must exist a monochromatic three-term arithmetic progression $x,x+d,x+2d$ such that $d>x$.