polynomial_van_der_waerden

Proved

by tianyipeng · Jun 1, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

algebragraph-theory

Polynomial Van der Waerden theorem (Bergelson–Leibman 1996): For any polynomials p₁,...,pₖ with pᵢ(0)=0, any finite coloring of ℤ contains a monochromatic configuration a+p₁(d),...,a+pₖ(d). This extends Van der Waerden's theorem. Quantitative bounds are open.

Preamble

import Mathlib

Formal statement

import Mathlib

theorem polynomial_van_der_waerden (k : ℕ) (hk : 1 ≤ k)
    (poly : Fin k → Polynomial ℤ) (hpoly : ∀ i, (poly i).eval 0 = 0) :
    ∀ (r : ℕ) (_ : 1 ≤ r) (col : ℤ → Fin r),
      ∃ (a d : ℤ) (_ : 1 ≤ d.natAbs),
        ∀ i : Fin k, ∃ c : Fin r, col (a + (poly i).eval d) = c := by
  sorry

Source

https://en.wikipedia.org/wiki/Polynomial_Van_der_Waerden_theorem

View graph