---

Claim. For every $k\ge1$, $W(k+1)\ge W(k)+k$, where $W(k)$ is the two-color van der Waerden number of Problem 138; hence $W(k+1)-W(k)\to\infty$, the second of the two questions Erdős asked in [Er81] and recorded in the problem's commentary (the first, whether $W(k+1)/W(k)\to\infty$, is not answered). The result is a Lean proof found by the DeepMind prover agent, the system named as the thread post and the formal-conjectures file name it, and posted on the site's thread on 2026-04-10 by Adam Zsolt Wagner with an informal account of the argument. The statement proved is erdos_138.variants.difference of the formal-conjectures file for the problem, that $W(k+1)-W(k)\to\infty$ with the answer True, where W is formal-conjectures' own van der Waerden number, the infimum of the $N$ such that every two-coloring of $\{1,\ldots,N\}$ has a monochromatic $k$-term arithmetic progression.

Submission note. Posted to the site's forum by Adam Zsolt Wagner on 10 April 2026:

The DeepMind prover agent has found a Lean proof for the difference variant as formalised in Formal Conjectures. Formal proof here.

An informal description of the proof is as follows. The argument is rather simple, once one knows what the right thing to prove is.

$Claim$: $W(k+1) \geq W(k) + k$

$Proof$: Given a 2-coloring 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 colored up to $M$ (where $M < W(k)-1+k$); we simply color $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 coloring 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$-APs, 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 colored red and blue, which is a contradiction.

Argument, in outline. As the thread post describes it: a two-coloring of $\{1,\ldots,W(k)-1\}$ with no monochromatic $k$-term progression is extended greedily by $k$ further integers, each colored red unless that closes a red $(k+1)$-term progression, and blue otherwise. Both choices can be blocked only by a red and a blue $k$-term progression whose next terms are the new integer; each of them contains a newly added element, so both common differences are below $k$, and stepping back $d_B$ terms along the red one and $d_R$ terms along the blue one lands on the same positive integer, which would have to carry both colors. The argument was not reconstructed in this corpus.

Covers. The question $W(k+1)-W(k)\to\infty$ of [Er81], through the explicit bound $W(k+1)\ge W(k)+k$. Not covered: the problem's own request, a bound on $W(k)$ itself or $W(k)^{1/k}\to\infty$, and the quotient question $W(k+1)/W(k)\to\infty$. On the thread the site's curator noted the generalization $W(k+1,l+1)\ge W(k,l)+\min(k,l)$ and a first $r$-color bound $W_r(k+1)-W_r(k)\ge k+r-1$, and Nat Sothanaphan linked notes, written with GPT-5.4 Thinking, refining the latter to $W_r(k+1)-W_r(k)\ge k+\min(k,F(r))+1$ with an explicit $F(r)=\Theta(r\log\log r)$; they have their own claim page.

Depends on. No page of this wiki; the proof is self-contained above Mathlib and formal-conjectures' definitions.

Standing. Claimed. The Lean proof is in a fork of formal-conjectures, the file linked above at two commits of 2026-04-10, the first the thread post's link and the second the one that the formal_proof attribute of the formal-conjectures file names; it proves the theorem from the lemma W_diff_tendsto, with no sorry in the theorem's proof, and the formal-conjectures file at its commit of 2026-10-06 marks the variant research solved with that pointer and the docstring that the DeepMind prover agent found a formal proof of the statement. Tsoukalas et al., Advancing Mathematics Research with AI-Driven Formal Proof Search (arXiv:2605.22763, 21 May 2026), is the paper the formal-conjectures file cites for the agent. The site's curator, Thomas Bloom, records the bound in the problem's commentary and credits DeepMind, but the site labels the problem OPEN, so that commentary is not acceptance, and no refereed publication of the result exists. This corpus has not built or audited the Lean proof, so the page lists no formalized evidence.