Erdős #138 — does W(k)^{1/k} → ∞ for van der Waerden numbers?

Statement

Let the van der Waerden number $W(k)$ be the least $N$ such that whenever $N\geq W(k)$ and $\{1,\ldots,N\}$ is 2-coloured, there must exist a monochromatic $k$-term arithmetic progression (this $N$ exists by van der Waerden's theorem). Improve the bounds for $W(k)$ — in particular, is it true that $$W(k)^{1/k}\to\infty \text{ as } k\to\infty?$$ (Erdős also separately asked the weaker question of whether $W(k)/2^k\to\infty$.)

Facts

- Prize \$500; status open, erdosproblems.com/138 tooltip: "This is open, and cannot be resolved with a finite computation" (site-owner belief, disclaimer applies). - Falsifiable: no — this is an asymptotic-growth-rate statement over all $k$, not a single checkable instance; needs a genuine proof or disproof. - Origin: raised across [Er57] [Er61] [Er73] [Er74b] [Er75b] [Er77c] [ErGr79] [Er80,p.90] [ErGr80] [Er81] [Er97c]; the \$500 offer for $W(k)^{1/k}\to\infty$ specifically is in Erdős, *A survey of problems in combinatorial number theory*, Ann. Discrete Math. (1980), 89–115 [Er80]. In [Er81] Erdős additionally asked whether $W(k+1)/W(k)\to\infty$ or (weaker) $W(k+1)-W(k)\to\infty$. - Best known upper bound: Gowers, *A new proof of Szemerédi's theorem*, Geom. Funct. Anal. (2001) 465–588 [Go01] — via a hypergraph-regularity / Gowers-uniformity-norm density-increment proof of Szemerédi's theorem, giving the explicit tower bound $$W(k)\leq 2^{2^{2^{2^{2^{k+9}}}}}.$$ This has not been improved for the general diagonal $W(k)$ since 2001 (per erdosproblems.com/138, current as of 2026-06-02 edit). - Best known general lower bound: Kozik and Shabanov, *Improved algorithms for colorings of simple hypergraphs and applications*, J. Combin. Theory Ser. B (2016) 312–332, arXiv:1409.6921 [KoSh16] — a random-recoloring (algorithmic Lovász Local Lemma) argument on simple hypergraph colourings proves $W(k,r) > c\cdot r^{k-1}$ for an absolute constant $c>0$; for $r=2$ this gives $W(k)\gg 2^k$. This is only $\Theta(2^k)$, i.e. it gives $W(k)^{1/k}\to 2$, a *bounded* limit — it does not resolve the \$500 question, and in fact together with Gowers' upper bound it shows the truth is sandwiched between exponential and tower-exponential in $k$, with the exponent-growth question wide open. (Predecessor: Berlekamp, *A construction for partitions which avoid long arithmetic progressions*, Canad. Math. Bull. (1968) 409–414 [Be68], proved the prime-indexed case $W(p+1)\geq p\cdot 2^p$ via an explicit finite-field construction; Szabó, *An application of Lovász' local lemma — a new lower bound for the van der Waerden number* (1990), gave $W(k)\geq 2^k/k^\varepsilon$ for any $\varepsilon>0$ and $k$ large, via the (non-algorithmic) symmetric Lovász Local Lemma — noted in the forum comments by Alfaiz/JakeMallen, 2025-12-01/28.) - Partial resolution of the difference-sub-question [Er81]: the DeepMind prover agent found a Lean proof (in google-deepmind/formal-conjectures) that $W(k+1)\geq W(k)+k$, via a short greedy-extension argument (extend an optimal $k$-AP-free 2-colouring of $[1,W(k)-1]$ by $k$ more points, colouring each new point to avoid completing a mono $(k+1)$-AP; a collision is impossible because two length-$\le(k-1)$-step APs of length $k$ sharing start/end point must share an interior point too). Posted/discussed by Adam Zsolt Wagner and Thomas Bloom on 2026-04-10 (erdosproblems.com/forum/discuss/138). Bloom immediately generalized it to $W(k+1,l+1)\geq W(k,l)+\min(k,l)$ and to a naive multicolour bound $W_r(k+1)-W_r(k)\geq k+r-1$; Nat Sothanaphan (with "GPT-5.4 Thinking", per the comment, 2026-04-10) refined this to $W_r(k+1)-W_r(k)\geq k+\min(k,F(r))+1$ with $F(r)=\Theta(r\log\log r)$. This answers only the weaker difference variant, not the ratio variant $W(k+1)/W(k)\to\infty$ (still open) and not the \$500 question $W(k)^{1/k}\to\infty$ (still open). - The Lean file FormalConjectures/ErdosProblems/138.lean confirms all this precisely: erdos_138 (the $500 question itself) is answer(sorry) — open; erdos_138.variants.quotient ($W(k+1)/W(k)\to\infty$) is answer(sorry) — open; erdos_138.variants.dvd_two_pow ($W(k)/2^k\to\infty$) is answer(sorry) — open; erdos_138.variants.difference is answer(True) — solved (the DeepMind result above); Berlekamp's and Gowers' bounds are tagged category research solved but their Lean *proofs* are still sorryd (stated, not yet formalized). - The $r\geq3$-colour analogue of the exact \$500 question is now resolved, and resolved in the *super*-exponential direction: Fox and Hunter, *Three-color van der Waerden numbers grow super-exponentially*, arXiv:2606.02541 (June 2026) [FoHu26], prove $w(k;3)$-type bounds beyond any exponential in $k$ — specifically a 3-colouring of $\{1,\ldots,2^{k(\log^*k)/4}\}$ with no monochromatic $k$-AP, so the 3-colour analogue of "$W(k)^{1/k}\to\infty$" is now a theorem. Predecessor multicolour work: Hunter, *Lower bounds for multicolor van der Waerden numbers*, Israel J. Math. (2025) [Hu25b], and Hunter, arXiv:2301.06212, *Lower bounds for multicolor van der Waerden numbers* (exponential improvement for $r\geq5$). - Closely related off-diagonal 2-colour question (different exponent regime): it was long conjectured/observed computationally that $w(3,k)=O(k^2)$ (avoid a 3-AP in colour 1 and a $k$-AP in colour 2). This was disproved by Ben Green, arXiv:2102.01543 (2021) — a random-quadratic-form pseudorandom construction gives $w(3,k)\geq k^{b(k)}$, $b(k)=c(\log k/\log\log k)^{1/3}$, superpolynomial; improved by Hunter, arXiv:2111.01099 (2021), to $b(k)=c\log k/\log\log k$ via an elementary probabilistic replacement for Green's random-quadratic-form step; a short direct $\Omega(k^2)$ proof is in Hunter, arXiv:2209.07651. Upper-bound side: Schoen, arXiv:2006.02877 (2020), $w(3,k)\leq\exp(O(k^{1-c}))$, subexponential. - **Sibling "canonical Ramsey" problem Erdős #190 — canonical Ramsey growth rate H(k)^{1/k}/k → ∞ (SOLVED) is fully SOLVED (2026): $H(k)$ = least $N$ such that every finite colouring of $[N]$ has a monochromatic or rainbow $k$-AP; Erdős–Graham [ErGr79,ErGr80] asked $H(k)^{1/k}/k\to\infty$. Resolved via the pigeonhole reduction $H(k)\geq W(k-1,k)$ combined with letting the colour count grow with $k$: Bae, arXiv:2604.20588 (2026) [Ba26], proves $H(k)\geq k^{(2-o(1))k}$ using the Erdős–Lovász LLL bound $W(r,k)\gg r^{k-1}/k$ applied with $r_0=\lfloor k/\log k\rfloor$ growing colours, the Blankenship–Cummings–Taranchuk recurrence, and the Baker–Harman–Pintz prime-gap theorem; Fox–Hunter arXiv:2606.02541 §6 independently get the stronger $H(k)\geq k^{(1-o(1))k\log k}$. The key trick — grow the number of colours with $k$ — is exactly what is unavailable for #138, which is fixed at $r=2$ colours; this is the structural reason #190's resolution does not transfer.** - OEIS A005346 records computed/known small values of $W(k)$. - Formalized in Lean: yes (statement only, not full proof) — google-deepmind/formal-conjectures/FormalConjectures/ErdosProblems/138.lean. - Related problems: Erdős #190 — canonical Ramsey growth rate H(k)^{1/k}/k → ∞ (SOLVED) (SOLVED sibling, canonical Ramsey growth rate), erdos/1030 (OPEN sibling, asks for a similar "gap grows" statement for consecutive Ramsey numbers $R(k+1,k)/R(k,k)>1+c$, flagged as an analogy by Bloom in the #138 comments).

Literature state

Not resolved for $r=2$ colours (the actual problem). As of the 2026-06-02 site edit and this search (2026-07-02), no proof or disproof of $W(k)^{1/k}\to\infty$ exists in the literature. The gap between the best lower bound ($\Theta(2^k)$, Kozik–Shabanov 2016, arXiv:1409.6921) and best upper bound (tower-of-five exponentials, Gowers 2001) has not narrowed on the exponent-growth-rate question specifically since these results; recent activity (2020s–2026) has instead resolved the *analogous* questions in adjacent settings: 1. The fixed-difference sub-question $W(k+1)-W(k)\to\infty$ [Er81] — solved 2026-04, DeepMind-generated Lean proof plus human refinements (Wagner/Bloom/Sothanaphan+GPT-5.4), via a short greedy/pigeonhole argument. Genuinely new technique for this family, but structurally weaker than the ratio or $1/k$-power questions. 2. The 3-colour diagonal analogue of the exact \$500 question — solved 2026-06, Fox–Hunter arXiv:2606.02541, super-exponential growth via an iterated/recursive construction exploiting $\log^* k$. 3. The canonical-Ramsey sibling Erdős #190 — canonical Ramsey growth rate H(k)^{1/k}/k → ∞ (SOLVED) — solved 2026 (Bae arXiv:2604.20588; Fox–Hunter §6), via letting the number of colours grow with $k$ ($r_0=k/\log k$) in the Erdős–Lovász LLL lower bound, which is precisely the freedom the 2-colour diagonal problem #138 does not have. 4. The off-diagonal 2-colour $w(3,k)$ question — a long-conjectured $O(k^2)$ polynomial bound was disproved (superpolynomial lower bound) by Green 2021/Hunter 2021/2022, via random-quadratic-form pseudorandom constructions — a genuinely new "arm" for beating naive Behrend/greedy lower-bound constructions in this family, but not yet ported back to the strictly-diagonal $W(k)$. No AI system (LLM, AlphaEvolve, Aristotle, etc.) is credited with progress on the core $500 question itself; DeepMind's contribution (item 1 above) is real but targets a strictly weaker sub-question that Erdős explicitly separated from the main $500 ask.

Attack surface

- Mode: literature-resolution + derivation (not finite-search; the site explicitly marks this as requiring an infinite/asymptotic argument, not a finite computation). - Concrete first experiment: (a) attempt to port Ben Green's random-quadratic-form pseudorandom construction (arXiv:2102.01543, refined by Hunter arXiv:2111.01099) from the off-diagonal $w(3,k)$ setting to the diagonal $W(k)=W_2(k)$ setting — check whether the same random-quadratic-residue colouring, or a genuinely 2-colour variant of it, can beat the $\Theta(2^k)$ Kozik–Shabanov barrier; this is a concrete, well-defined "read the two papers closely and check where the off-diagonal structure ($k$-AP vs $3$-AP asymmetry) was load-bearing" task. (b) Separately, formalize in Lean the Kozik–Shabanov and Gowers bounds (currently sorryd in FormalConjectures/ErdosProblems/138.lean) to get a machine-checked floor/ceiling before attempting new bounds — cheap, concrete, and directly extends the existing DeepMind/formal-conjectures effort on this exact file. - Oracle: none for the core asymptotic claim itself (unfalsifiable by finite means, per the site). For sub-experiment (a): any claimed new construction is checked the same way Green/Hunter's are — an explicit lower-bound proof for a specific colouring family, checkable by hand/computer-algebra for small $k$ as a sanity check even though the asymptotic claim itself needs a proof. For sub-experiment (b): Lean compilation is the oracle. - Feasibility: honest read — famous and hard, but with a genuinely fresh, recently-opened line of attack. The core \$500 question has resisted improvement on either bound since 2016 (lower) / 2001 (upper). However, 2026 saw *three* closely-related sibling questions resolved in quick succession (April: difference variant; June: 3-colour diagonal via Fox–Hunter; also June: canonical-Ramsey via Bae) by techniques that are each structurally blocked from transferring directly to #138 (growing colour count doesn't apply at fixed $r=2$; the 3-colour super-exponential construction's $\log^* k$ trick is specific to having a 3rd colour to "sacrifice" for iteration/recursion — worth checking in detail whether Fox–Hunter's technique has *any* 2-colour residue). This makes #138 a good candidate to revisit *now*, specifically by reading Fox–Hunter arXiv:2606.02541 in full (not just the abstract) to see if their iterated/log* construction has a 2-colour analogue, since it is the most recent and most powerful new machinery in this exact problem family.

Related

- Erdős #190 — canonical Ramsey growth rate H(k)^{1/k}/k → ∞ (SOLVED) — "canonical Ramsey" sibling ($H(k)^{1/k}/k\to\infty$), fully SOLVED 2026 via growing-colour-count Lovász Local Lemma + Baker–Harman–Pintz prime gaps (Bae arXiv:2604.20588) and independently via Fox–Hunter arXiv:2606.02541 §6; the winning trick (let $r\to\infty$ with $k$) is structurally unavailable for #138's fixed-$r=2$ setting — the clearest "near miss" analog. - erdos/1030 — open sibling asking for a similar asymptotic-gap statement for consecutive Ramsey numbers, $R(k+1,k)/R(k,k)>1+c$; flagged by Thomas Bloom in the #138 forum comments (2026-04-10) as a graph-theoretic analogue with no known common proof technique, since the "two APs of length $k$ sharing an interior point" fact used for the $W(k+1)\geq W(k)+k$ argument has no graph-theoretic counterpart. - Lovász Local Lemma (symmetric, general/asymmetric, and algorithmic/random-recoloring variants) — probabilistic existence when bad events are individually non-negligible but sparsely dependent — Szabó (1990, symmetric LLL) and Kozik–Shabanov (arXiv:1409.6921, algorithmic/random-recoloring LLL) both derive the current-best $\Omega(2^k)$ lower bound this way. - Hypergraph regularity / Gowers uniformity norms and density-increment arguments: quasirandom decomposition + counting/removal lemmas, and the iterative-density-increase route to Szemerédi-type theorems — Gowers' arXiv-era (GAFA 2001) proof of Szemerédi's theorem via hypergraph/Gowers-uniformity-norm density increment, source of the current tower-type upper bound on $W(k)$. - Greedy pointwise-extension argument exploiting shared interior points of APs — the DeepMind/Wagner/Bloom proof that $W(k+1)\geq W(k)+k$, exploiting that two length-$k$ APs of step $<k$ sharing endpoints must share an interior point. - Random quadratic form pseudorandom coloring constructions (Green–Hunter annulus method) — Ben Green's (arXiv:2102.01543) pseudorandom lower-bound construction that disproved the conjectured $O(k^2)$ bound for off-diagonal $w(3,k)$; refined by Hunter (arXiv:2111.01099); candidate technique to try porting to the diagonal $W(k)$. - Log*-depth iterated/recursive lower-bound constructions (self-similar amplification budgeted by the inverse tower function) — Fox–Hunter's (arXiv:2606.02541) super-exponential 3-colour construction using an iterated/recursive scheme with a $\log^*k$-depth recursion; the newest, most powerful machinery in this problem family, not yet checked for a 2-colour residue. - Lean 4 formalization of constructions and conditional reductions (Erdős-problem context) — google-deepmind/formal-conjectures/FormalConjectures/ErdosProblems/138.lean; the \$500 question and two sub-variants are answer(sorry), the difference-variant is answer(True) (DeepMind-proved), Berlekamp/Gowers bounds are stated but their proofs are sorryd — a concrete formalization target independent of resolving the open question.