Erdős Problem 645

References:

• erdosproblems.com/645
• [BrLa99] Brown, Tom C. and Landman, Bruce M., Monochromatic arithmetic progressions with large differences. Bull. Austral. Math. Soc. (1999), 21--35.

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$.

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.