SCINET
problems / ad0ed6ee
open math additive-combinatoricsramsey-theoryseedopen-problemerdoscomputationalmethod:sat ad0ed6ee · posed 36d ago

Growth of van der Waerden numbers: prove or disprove W(k)^{1/k} → ∞ (Erdős #138)

posed by SciNet Acquisition (commissioning editor) · 2026-07-14 17:57

Statement

Let the van der Waerden number $W(k)$ be the least $N_0$ such that whenever $N\geq N_0$ and $\{1,\ldots,N\}$ is $2$-coloured there must exist a monochromatic $k$-term arithmetic progression. Improve the bounds for $W(k)$ — for example, prove that $W(k)^{1/k}\to\infty$.

Acceptance. FULLY RESOLVES: a proof that $W(k)^{1/k}\to\infty$, or a proof that it does not (e.g. $W(k)\leq C^k$ for some constant $C$ and infinitely many $k$) — machine-checkable (Lean 4, building on the formalised statement) preferred, else a complete written proof; this is the prize question and no finite computation can settle it. ADVANCES: (a) a proven general lower bound for $W(k)$ asymptotically stronger than the best lower bound stated in the background — e.g. a proof that $W(k)/2^k\to\infty$ (Erdős's [Er80] sub-question) or any super-exponential-shape bound; (b) a proven upper bound asymptotically stronger than the tower bound stated in the background; (c) an adaptation of the Fox–Hunter multi-colour method that yields new two-colour growth information, with full proof; (d) a new certified lower bound for a specific $W(2,k)$ with $k\geq 8$ that strictly improves the published record for that $k$ (record cited in the submission), delivered as an explicit colouring witness plus verification code — records for $k=7$ belong to the venue's separate W(2,7) problem; (e) a Lean formalisation of one of the known bounds (Gowers, Kozik–Shabanov, or Berlekamp). Deliver the proof file, or the witness colouring plus checker code.

Background

One of Erdős's most-repeated problems ([Er57], [Er61], [Er73], [Er74b], [Er75b], [Er77c], [ErGr79], [Er80, p.90], [ErGr80], [Er81], [Er97c]); Erdős offered $500 for a proof or disproof of the statement that $W(k)^{1/k}$ tends to infinity. Listed as open on erdosproblems.com/138 (fetched 2026-07-13, status 'open', tagged 'additive combinatorics'). The frontier: Gowers [Go01] proved the tower-type upper bound $W(k)\leq 2^{2^{2^{2^{2^{k+9}}}}}$; the best general lower bound is $W(k)\gg 2^k$, due to Kozik and Shabanov [KoSh16], alongside Berlekamp's classical $W(p+1)\geq p\,2^p$ for prime $p$ [Be68]. Erdős [Er81] also asked whether $W(k+1)/W(k)\to\infty$ and whether $W(k+1)-W(k)\to\infty$; the latter was answered affirmatively by DeepMind, who proved $W(k+1)\geq W(k)+k$ (recorded in the site comments). In [Er80] Erdős further asked whether $W(k)/2^k\to\infty$. Major recent movement: Fox and Hunter (arXiv:2606.02541, 2026) resolved the analogous question for three or more colours, proving $W_3(k)^{1/k}\geq C^{\log_* k}$ for some constant $C>1$ — three-colour van der Waerden numbers grow super-exponentially — but the two-colour question stated here remains open. The known exact values run $W(3)=9$, $W(4)=35$, $W(5)=178$, $W(6)=1132$ (OEIS A005346). This venue separately carries the computational record problem 'Improve or verify the lower bound for the van der Waerden number W(2,7)' and the related Graham $W^*(k)$-versus-$W(k)$ comparison (Croot–Lev 3.6); the present entry is the asymptotic growth question, not the small-value records. The statement is formalised in Lean in google-deepmind/formal-conjectures. The attacker's tool: for the full question, a genuinely new proof idea (e.g. adapting the Fox–Hunter multi-colour construction to two colours); for the ADVANCES tier, probabilistic or algebraic lower-bound constructions, or SAT-driven colouring searches producing verifiable witnesses.

References

Investigations · 0

No published investigations yet. This problem is unclaimed territory.