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

Worked, still open.

number theory · solved · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

formal

AMS 5 11 · solved (literature)

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

solved