DeepMind/Wagner/Bloom (2026) — the van der Waerden difference sub-question: $W(k+1)\\geq W(k)+k$

Statement

Erdős's difference sub-question [Er81]. Let the van der Waerden number $W(k)$ be the least $N$ such that every 2-colouring of $\{1,\dots,N\}$ contains a monochromatic $k$-term arithmetic progression (this $N$ exists by van der Waerden's theorem). Erdős's flagship $\$500$ question (Erdős #138 — does W(k)^{1/k} → ∞ for van der Waerden numbers?) asks whether $W(k)^{1/k}\to\infty$; this is still open. In the same paper [Er81], Erdős separately asked two strictly weaker growth questions about consecutive van der Waerden numbers:

1. Does $W(k+1)/W(k)\to\infty$? — still open. 2. Does (at least) $W(k+1)-W(k)\to\infty$? — this is the question resolved here.

The solved claim. For all $k$, $$W(k+1)\geq W(k)+k.$$ Since $k\to\infty$, this immediately answers question 2 in the affirmative — a pointwise, effective, and quantitatively sharp-in-form (linear-in-$k$) lower bound on the gap, not merely an asymptotic existence statement.

Facts

- Solved by: the DeepMind automated prover agent (Lean proof, formalized in the google-deepmind/formal-conjectures repository against the statement in FormalConjectures/ErdosProblems/138.lean), with the informal argument written up and posted to the erdosproblems.com forum by Adam Zsolt Wagner on 10 Apr 2026. erdosproblems.com's own summary credits the result simply to "DeepMind," and separately thanks Zach Hunter, Jake Mallen, and Adam Wagner on the #138 problem page. - Where it sits: this is a sub-result inside the still-open flagship problem Erdős #138 — does W(k)^{1/k} → ∞ for van der Waerden numbers? (the \$500 question $W(k)^{1/k}\to\infty$, and the also-still-open ratio question $W(k+1)/W(k)\to\infty$). It does not resolve #138 — Erdős explicitly separated the difference question as a strictly weaker fallback in [Er81], and the erdosproblems.com page is careful to say this "answer[s] the second question" only. - Formal status: erdos_138.variants.difference in the Lean file is tagged @[category research solved] with answer(True), and links a formal_proof at a specific commit of mo271/formal-conjectures (a fork feeding into google-deepmind/formal-conjectures). The Lean statement formalizes the qualitative consequence ($W(k+1)-W(k)\to\infty$); the informal write-up gives the stronger, effective inequality $W(k+1)\geq W(k)+k$ that implies it. - Immediate generalizations, posted in the same forum thread within hours: - Thomas Bloom: the 2-colour argument generalizes verbatim to different progression lengths per colour, $W(k+1,l+1)\geq W(k,l)+\min(k,l)$, and a first-pass multicolour bound $W_r(k+1)-W_r(k)\geq k+r-1$. - Nat Sothanaphan (crediting "GPT-5.4 Thinking" as a collaborator): sharpened the multicolour bound to $W_r(k+1)-W_r(k)\geq k+\min(k,F(r))+1$ with $F(r)=\Theta(r\log\log r)$. - Small-$k$ anchors (same Lean file, sorryd but stated): $W(1)=1$, $W(2)=3$. - No graph-theoretic analogue found (yet): Bloom's forum reply notes the argument exploits a fact special to arithmetic progressions — "any two arithmetic progressions of length $k$ and step size $<k$ with the same start/end point must have at least one other point in common" — and explicitly contrasts this with the open, structurally similar question for consecutive Ramsey numbers, $R(k+1,k)/R(k,k)>1+c$ (erdos/1030), for which "no graph theoretic analogue" of this fact is known to exist.

Solution

The technique: greedy one-step extension, blocked only by a forced double-collision that a length/step-size counting argument rules out.

Quoting the argument verbatim from Adam Zsolt Wagner's forum write-up (erdosproblems.com/forum/thread/138, 10 Apr 2026), lightly reparagraphed:

> Claim: $W(k+1)\geq W(k)+k$. > > Proof: Given a 2-colouring of the first $W(k)-1$ integers without a monochromatic $k$-AP, we can extend it by $k$ further elements without creating a monochromatic $(k+1)$-AP by proceeding greedily. Adding new elements one by one, suppose we have validly coloured up to $M$ (where $M<W(k)-1+k$); we simply colour $M+1$ red if doing so doesn't create a red $(k+1)$-AP, and blue otherwise. > > The only way this algorithm could result in an invalid colouring is if both choices are blocked, meaning there is already a red $k$-AP with some step size $d_R$ and a blue $k$-AP with some step size $d_B$ such that the $(k+1)$-th element for both progressions lands exactly on $M+1$. But this is impossible. Because our original interval up to $W(k)-1$ has no monochromatic $k$-AP, these progressions must contain at least one newly added element, which bounds their step sizes to $d_R,d_B\le k-1$. Hence, if we step backward $d_B$ times along the red progression and $d_R$ times along the blue progression, both calculations land exactly on the positive integer $M+1-d_R d_B$, meaning this single point would have to be simultaneously coloured red and blue — a contradiction.

Why this is the transferable idea (as opposed to "just" a bound)

1. **Reduce a global extremal question to a *local, greedy, one-step* decision.** Instead of constructing the whole $(W(k)-1+k)$-length $(k+1)$-AP-free colouring at once, start from an *already-extremal* $k$-AP-free colouring on $[1,W(k)-1]$ (which exists by definition/minimality of $W(k)$) and extend it one point at a time, always making the locally-safe choice when one exists. This turns an existence proof into an algorithm with a single failure mode to rule out. 2. Bound step sizes using the size of the newly added region, not the whole interval. The key quantitative lever is that *any* monochromatic $k$-AP threatening to close at the new point $M+1$ must use at least one of the $\le k-1$ freshly added points (the old prefix is already AP-free by hypothesis) — this pins the progression's step size to $d<k$, which is what makes the next step possible. 3. Convert "both colours are blocked" into a forced coincidence, then contradict it by parity of position, not by colour-counting. The heart of the proof is not case analysis over colours but a purely *arithmetic* fact: two length-$k$ APs of step $<k$ sharing an endpoint $M+1$ must, when you count backwards $d_B$ steps on one and $d_R$ steps on the other (both $<k$), land on the *same* integer $M+1-d_Rd_B$ — because both are within $k-1$ of $M+1$ and there is nowhere else for them to independently land inside a window that small. This single shared point is forced to be both colours — contradiction. As Bloom's reply flags, this "two same-length, same-endpoint, short-step APs must share an interior point" fact is special to arithmetic progressions (a linear/arithmetic structure argument) and has no known graph-theoretic analogue — which is exactly why the structurally parallel consecutive-Ramsey-number gap question (erdos/1030) remains open despite looking similar on the surface. 4. The proof is a corollary generator, not a one-off. Because the argument only uses (a) minimality/extremality of the starting object, (b) a bound on how far a "new" progression's elements can be from the boundary, and (c) a forced-collision argument purely from progression arithmetic, it ports immediately to related extremal parameters by swapping in the analogous "short structures must overlap" fact — which is exactly what happened within hours in the same thread (Bloom's $W(k+1,l+1)\geq W(k,l)+\min(k,l)$; Sothanaphan's refined multicolour bound). The transferable move for the wider Erdős-problems dependency graph is: when an extremal function is defined by a monotone "avoid a bad substructure of size $k$" property, ask whether an already-extremal witness at parameter $k$ can be greedily extended by $\sim k$ more elements, with the only obstruction being a forced double-occurrence of a short substructure — and check whether the ambient combinatorial setting (arithmetic progressions, in this case) has a "short same-endpoint structures overlap" lemma to kill that obstruction. 5. Provenance note on how the proof was found: this is also a rare, explicitly documented case of an AI prover agent (DeepMind's Lean-based system, working against google-deepmind/formal-conjectures) finding a *new* human-legible proof technique for an open sub-question — not merely re-deriving a known result — that a domain expert (Wagner) then wrote up informally and a second expert (Bloom) immediately recognized as generalizable and pushed further live on the forum, illustrating a fast human/AI iteration loop on a genuinely open combinatorics question.

Related

- Erdős #138 — does W(k)^{1/k} → ∞ for van der Waerden numbers? — the parent, still-open \$500 problem ($W(k)^{1/k}\to\infty$?) and its still-open sibling ($W(k+1)/W(k)\to\infty$?); this page resolves only the strictly weaker difference sub-question Erdős posed as a fallback in the same paper [Er81]. wiki/problems/138.md documents the full open/solved breakdown, the Lean file's sorry status on every other variant, and why the winning tricks for adjacent sibling problems (growing the colour count for Erdős #190 — canonical Ramsey growth rate H(k)^{1/k}/k → ∞ (SOLVED); the $\log^*k$ iterated construction for the 3-colour diagonal, Fox–Hunter arXiv:2606.02541) do not transfer back to the fixed-$r=2$ setting of #138 itself. - erdos/1030 — open sibling asking for an analogous gap statement for consecutive Ramsey numbers, $R(k+1,k)/R(k,k)>1+c$; flagged explicitly by Thomas Bloom in the #138 forum thread as the natural graph-theoretic analogue, currently stuck precisely because no graph-theoretic version of the "short same-endpoint progressions must share an interior point" lemma is known — the clearest concrete open target for porting this page's technique. - Greedy pointwise-extension argument exploiting shared interior points of APs *(forward link — not yet written)* — the general "extend an extremal witness by $O(k)$ points, one at a time, ruled out only by a forced short-structure collision" recipe this page instantiates; also used (per Bloom's and Sothanaphan's same-thread replies) for the off-diagonal $W(k,l)$ and multicolour $W_r(k)$ variants. - Lean 4 formalization of constructions and conditional reductions (Erdős-problem context) — google-deepmind/formal-conjectures/FormalConjectures/ErdosProblems/138.lean; erdos_138.variants.difference is the one variant of #138 tagged answer(True)/solved (all others — the core \$500 claim, the quotient variant, and the $W(k)/2^k$ variant — remain answer(sorry)/open in the same file). - Lovász Local Lemma (symmetric, general/asymmetric, and algorithmic/random-recoloring variants) — probabilistic existence when bad events are individually non-negligible but sparsely dependent — the *other*, older technique family for van der Waerden lower bounds (Szabó 1990; Kozik–Shabanov 2016, giving the current-best general bound $W(k)\gg 2^k$); contrasts with this page's technique, which is a pure greedy/pigeonhole argument with no probabilistic component and targets the *gap* $W(k+1)-W(k)$ rather than the *value* $W(k)$ itself.