Monochromatic progressions with large common difference

DefinitionErdős Problem 645#✓fully proved

The statement that for every colouring of the positive integers with two colours there are positive integers \(x\) and \(d\) with \(d > x\) such that \(x\), \(x + d\) and \(x + 2d\) all have the same colour.

def monochromaticProgressionLargeDifference : Prop :=
  ∀ c : ℕ → Bool, ∃ x d : ℕ, 0 < x ∧ x < d ∧ c x = c (x + d) ∧ c (x + d) = c (x + 2 * d)

Used by 1

Used byErdős Problem 645 is true

TheoremErdős Problem 645 is true#●ready to prove

For every colouring of the positive integers with two colours there are positive integers \(x\) and \(d\) with \(d > x\) such that \(x\), \(x + d\) and \(x + 2d\) all have the same colour.

Brown and Landman proved more: for every increasing function \(f\) there is such a monochromatic progression with \(d > f(x)\). Erdős Problems also records a short argument of Alweiss.

public theorem_wanted monochromaticProgressionLargeDifference_holds :
    monochromaticProgressionLargeDifference

Sources

• T. F. Bloom, Erdős Problems, Problem #645, https://www.erdosproblems.com/645 (status PROVED (LEAN)); resolution: T. C. Brown and B. M. Landman, Monochromatic arithmetic progressions with large differences, Bull. Austral. Math. Soc. (1999), 21-35, erdosproblems.com/645: first proved by Brown and Landman, with d > f(x) for any increasing f; the page records a short argument of Alweiss, https://www.erdosproblems.com/645.

Uses 1

Statement usesErdős Problem 645

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.