Erdős problem 645

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

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

645.lean

Retained formal statement1 of 1

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.

FormalConjectures/ErdosProblems/645.leanErdos645.erdos_6451 lineExact file

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

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.