Erdős Problem 645

Theorem 645 · Erdős

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

This was first proved by Brown and Landman [BrLa99], who in fact show that this is always possible with $d>f(x)$ for any increasing function $f$ .

This was formalized in Lean by Alexeev using Aristotle and ChatGPT.

Formal statement · Lean 4.lean

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

Proof. sorry

Nobody has tried yet.