Van der Waerden numbers W(3, k)

DefinitionMonochromatic arithmetic progression#✓fully proved

Let \(c\) be a colouring of the natural numbers with the two colours true and false, let \(b\) be a colour and let \(l, N\) be natural numbers. Then \(c\) has a monochromatic progression of colour \(b\) and length \(l\) in \(\{1, \dots, N\}\) when there are natural numbers \(a \ge 1\) and \(d \ge 1\) with \(a + (l - 1) d \le N\), where \(l - 1\) is read as \(0\) when \(l = 0\), such that \(c(a + j d) = b\) for every \(j < l\).

def HasMonochromaticAP (c : ℕ → Bool) (b : Bool) (l N : ℕ) : Prop :=
  ∃ a d : ℕ, 1 ≤ a ∧ 1 ≤ d ∧ a + (l - 1) * d ≤ N ∧ ∀ j < l, c (a + j * d) = b

Used by 1

Used byPolynomial growth of the off-diagonal van der Waerden numbers (claim)

DefinitionPolynomial growth of the off-diagonal van der Waerden numbers (claim)#✓fully proved

There are natural numbers \(C\) and \(A\) such that for every \(k \ge 1\), every colouring of the natural numbers in red and blue has a red \(3\)-term or a blue \(k\)-term arithmetic progression \(a, a + d, \dots\) with \(a \ge 1\), \(d \ge 1\) and all terms in \(\{1, \dots, C k^A\}\). Equivalently, the van der Waerden number \(W(3, k)\), the least \(n\) such that every red/blue colouring of \(\{1, \dots, n\}\) has a red \(3\)-term or a blue \(k\)-term arithmetic progression, satisfies \(W(3, k) \le C k^A\) for every \(k \ge 1\).

This is the AIM question (Graph Ramsey theory, Problem 43) stated as a claim.

def offDiagonalVanDerWaerdenPolynomial : Prop :=
  ∃ C A : ℕ, ∀ k : ℕ, 1 ≤ k → ∀ c : ℕ → Bool,
    HasMonochromaticAP c true 3 (C * k ^ A) ∨ HasMonochromaticAP c false k (C * k ^ A)

Uses 1 · Used by 1

Statement usesMonochromatic arithmetic progression

Used byThe off-diagonal van der Waerden numbers are not polynomially bounded

TheoremThe off-diagonal van der Waerden numbers are not polynomially bounded#●ready to prove

There are no natural numbers \(C\) and \(A\) such that for every \(k \ge 1\), every colouring of the natural numbers in red and blue has a red \(3\)-term or a blue \(k\)-term arithmetic progression \(a, a + d, \dots\) with \(a \ge 1\), \(d \ge 1\) and all terms in \(\{1, \dots, C k^A\}\).

Equivalently, the van der Waerden number \(W(3, k)\), the least \(n\) such that every red/blue colouring of \(\{1, \dots, n\}\) has a red \(3\)-term or a blue \(k\)-term arithmetic progression, is not bounded by \(C k^A\) for any constants \(C\) and \(A\). Green proved that for some constant \(c > 0\) and all sufficiently large \(k\), \(W(3, k) \ge k^{b(k)}\) with \(b(k) = c (\log k / \log \log k)^{1/3}\), which tends to infinity (the colours of his colouring are swapped relative to this statement, which is symmetric).

public theorem_wanted offDiagonalVanDerWaerdenPolynomial_refuted :
    ¬ offDiagonalVanDerWaerdenPolynomial

Sources

• AIM workshop Graph Ramsey theory, problem list, https://www.overleaf.com/read/mnvcscjjysvg, Problem 43 (same text: AimPL, Graph Ramsey Theory, section 25, http://aimpl.org/graphramsey/1/); resolution: B. Green, New lower bounds for van der Waerden numbers, Forum Math. Pi 10 (2022), e18, arXiv:2102.01543, abstract and main theorem: there is a red-blue colouring of [N] with no blue 3-term progression and no red progression of length e^{C (log N)^{3/4} (log log N)^{1/4}}, so w(3, k) ≥ k^{b(k)} with b(k) = c (log k / log log k)^{1/3} → ∞; Z. Hunter (arXiv:2111.01099) improved this to w(3, k) ≥ k^{c log k / log log k}, https://doi.org/10.1017/fmp.2022.12.

Uses 1

Statement usesPolynomial growth of the off-diagonal van der Waerden numbers (claim)

DefinitionMonochromatic arithmetic progressions in an initial interval#✓fully proved

Let \(c\) be a red/blue colouring of the natural numbers, given as a map to the Booleans (\(\mathrm{true}\) is red, \(\mathrm{false}\) is blue), let \(b\) be a colour and let \(\ell\) and \(N\) be natural numbers. Then \(c\) has an \(\ell\)-term arithmetic progression of colour \(b\) inside \(\{1, \dots, N\}\) if there are natural numbers \(a\) and \(d > 0\) such that for every \(i < \ell\) we have \(1 \le a + id \le N\) and \(c(a + id) = b\).

def HasMonoAP (c : ℕ → Bool) (b : Bool) (ℓ N : ℕ) : Prop :=
  ∃ a d : ℕ, 0 < d ∧ ∀ i < ℓ, 1 ≤ a + i * d ∧ a + i * d ≤ N ∧ c (a + i * d) = b

Used by 1

Used byIntervals forcing the van der Waerden number \(W(3, k)\)

DefinitionIntervals forcing the van der Waerden number \(W(3, k)\)#✓fully proved

For natural numbers \(N\) and \(k\), the interval \(\{1, \dots, N\}\) forces \(W(3, k)\) if every red/blue colouring of the natural numbers has, inside \(\{1, \dots, N\}\), a red \(3\)-term arithmetic progression or a blue \(k\)-term arithmetic progression (progressions have common difference \(d > 0\)). Equivalently \(W(3, k) \le N\), where the van der Waerden number \(W(3, k)\) is the least \(n\) such that every red/blue colouring of \(\{1, \dots, n\}\) has a red \(3\)-term or a blue \(k\)-term arithmetic progression.

def ForcesThreeK (N k : ℕ) : Prop :=
  ∀ c : ℕ → Bool, HasMonoAP c true 3 N ∨ HasMonoAP c false k N

Uses 1 · Used by 2

Statement usesMonochromatic arithmetic progressions in an initial interval

Used bySubexponential upper bound for \(W(3, k)\) (statement) · Green's superpolynomial lower bound for \(W(3, k)\) (statement)

DefinitionSubexponential upper bound for \(W(3, k)\) (statement)#✓fully proved

Write \(W(3, k)\) for the van der Waerden number: the least \(n\) such that every red/blue colouring of \(\{1, \dots, n\}\) has a red \(3\)-term or a blue \(k\)-term arithmetic progression (progressions have common difference \(d > 0\)). Say that \(N\) forces \(W(3, k)\) if every red/blue colouring of \(\{1, \dots, N\}\) has a red \(3\)-term or a blue \(k\)-term arithmetic progression. This is the proposition that there is a real constant \(c < 1\) such that for all sufficiently large natural numbers \(k\) some natural number \(N < \exp(k^c)\) forces \(W(3, k)\). Equivalently, \(W(3, k) < \exp(k^c)\) for all large \(k\).

def vanDerWaerdenThreeSubexponential : Prop :=
  ∃ c : ℝ, c < 1 ∧ ∀ᶠ k : ℕ in Filter.atTop,
    ∃ N : ℕ, (N : ℝ) < Real.exp ((k : ℝ) ^ c) ∧ ForcesThreeK N k

Uses 1 · Used by 1

Statement usesIntervals forcing the van der Waerden number \(W(3, k)\)

Used bySchoen's subexponential upper bound for \(W(3, k)\)

DefinitionGreen's superpolynomial lower bound for \(W(3, k)\) (statement)#✓fully proved

Write \(W(3, k)\) for the van der Waerden number: the least \(n\) such that every red/blue colouring of \(\{1, \dots, n\}\) has a red \(3\)-term or a blue \(k\)-term arithmetic progression (progressions have common difference \(d > 0\)). Say that \(N\) forces \(W(3, k)\) if every red/blue colouring of \(\{1, \dots, N\}\) has a red \(3\)-term or a blue \(k\)-term arithmetic progression. This is the proposition that there is a real constant \(c > 0\) such that for all sufficiently large natural numbers \(k\), no natural number \(N < \exp\bigl(c (\log k)^{4/3} / (\log \log k)^{1/3}\bigr)\) forces \(W(3, k)\). Equivalently, \(W(3, k) \ge \exp\bigl(c (\log k)^{4/3} / (\log \log k)^{1/3}\bigr)\) for all large \(k\).

def vanDerWaerdenThreeSuperpolynomial : Prop :=
  ∃ c : ℝ, 0 < c ∧ ∀ᶠ k : ℕ in Filter.atTop, ∀ N : ℕ,
    (N : ℝ) < Real.exp (c * Real.log k ^ ((4 : ℝ) / 3) / Real.log (Real.log k) ^ ((1 : ℝ) / 3)) →
      ¬ ForcesThreeK N k

Uses 1 · Used by 1

Statement usesIntervals forcing the van der Waerden number \(W(3, k)\)

Used byGreen's superpolynomial lower bound for \(W(3, k)\)

TheoremSchoen's subexponential upper bound for \(W(3, k)\)#●ready to prove

Write \(W(3, k)\) for the van der Waerden number: the least \(n\) such that every red/blue colouring of \(\{1, \dots, n\}\) has a red \(3\)-term or a blue \(k\)-term arithmetic progression (progressions have common difference \(d > 0\)). Say that \(N\) forces \(W(3, k)\) if every red/blue colouring of \(\{1, \dots, N\}\) has a red \(3\)-term or a blue \(k\)-term arithmetic progression. There is a real constant \(c < 1\) such that for all sufficiently large natural numbers \(k\) some natural number \(N < \exp(k^c)\) forces \(W(3, k)\). Equivalently, \(W(3, k) < \exp(k^c)\) for all large \(k\).

Schoen proved \(W(3, k) \le \exp(O(k^{1-\delta}))\) for an absolute constant \(\delta > 0\), which gives this statement; erdosproblems.com/721 records Schoen as the first to show it. The best known bound is now \(\exp(O((\log k)^9))\), via Bloom and Sisask.

public theorem_wanted vanDerWaerdenThreeSubexponential_holds : vanDerWaerdenThreeSubexponential

Sources

• T. F. Bloom, Erdős Problems, Problem #721, https://www.erdosproblems.com/721 (status SOLVED); resolution: T. Schoen, A subexponential upper bound for van der Waerden numbers W(3, k), Electron. J. Combin. 28 (2021), Paper 2.34; B. Green, New lower bounds for van der Waerden numbers, Forum Math. Pi 10 (2022), e18, Schoen's abstract: N ≤ exp(O(k^{1-c})) for an absolute c > 0 whenever {1, …, N} splits into a 3-AP-free part and a k-AP-free part; abstract of arXiv:2102.01543 (Green): w(3, k) ≥ k^{b(k)} with b(k) = c (log k / log log k)^{1/3}; erdosproblems.com/721: both specific challenges of Erdős have been met, https://www.combinatorics.org/ojs/index.php/eljc/article/view/v28i2p34.

Uses 1

Statement usesSubexponential upper bound for \(W(3, k)\) (statement)

TheoremGreen's superpolynomial lower bound for \(W(3, k)\)#●ready to prove

Write \(W(3, k)\) for the van der Waerden number: the least \(n\) such that every red/blue colouring of \(\{1, \dots, n\}\) has a red \(3\)-term or a blue \(k\)-term arithmetic progression (progressions have common difference \(d > 0\)). Say that \(N\) forces \(W(3, k)\) if every red/blue colouring of \(\{1, \dots, N\}\) has a red \(3\)-term or a blue \(k\)-term arithmetic progression. There is a real constant \(c > 0\) such that for all sufficiently large natural numbers \(k\), no natural number \(N < \exp\bigl(c (\log k)^{4/3} / (\log \log k)^{1/3}\bigr)\) forces \(W(3, k)\). Equivalently, \(W(3, k) \ge \exp\bigl(c (\log k)^{4/3} / (\log \log k)^{1/3}\bigr)\) for all large \(k\).

Green's colouring has no \(3\)-term progression in one colour and no long progression in the other; it disproves Graham's guess \(W(3, k) \ll k^2\). Hunter improved the bound to \(\exp(c (\log k)^2 / \log \log k)\) (erdosproblems.com/721).

public theorem_wanted vanDerWaerdenThreeSuperpolynomial_holds : vanDerWaerdenThreeSuperpolynomial

Sources

• T. F. Bloom, Erdős Problems, Problem #721, https://www.erdosproblems.com/721 (status SOLVED); resolution: T. Schoen, A subexponential upper bound for van der Waerden numbers W(3, k), Electron. J. Combin. 28 (2021), Paper 2.34; B. Green, New lower bounds for van der Waerden numbers, Forum Math. Pi 10 (2022), e18, Schoen's abstract: N ≤ exp(O(k^{1-c})) for an absolute c > 0 whenever {1, …, N} splits into a 3-AP-free part and a k-AP-free part; abstract of arXiv:2102.01543 (Green): w(3, k) ≥ k^{b(k)} with b(k) = c (log k / log log k)^{1/3}; erdosproblems.com/721: both specific challenges of Erdős have been met, https://www.combinatorics.org/ojs/index.php/eljc/article/view/v28i2p34.

Uses 1

Statement usesGreen's superpolynomial lower bound for \(W(3, k)\) (statement)

6 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.