---

Claim. The preprint Quantitative superexponential bounds for van der Waerden numbers of the OpenAI mathematics release (dated 23 September 2026, authored by OpenAI) states as its main theorem that there is an absolute integer $K_0$ such that for every $k\ge K_0$ and every $r\ge2$

$$W_r(k)>k^{ck\lfloor\log_2r\rfloor},\qquad c=10^{-5},$$

where $W_r(k)$ is the least $N$ such that every map $[N]\to[r]$ is constant on some $k$-term arithmetic progression inside $[N]$ (fewer than $r$ colors may be used). For two colors this is $W(k)>k^{k/100000}$ for all large $k$, so $W(k)^{1/k}\to\infty$, the question of Problem 138, which the manuscript names as its target; its introduction credits the earlier bounds of Berlekamp, Szabó, Kozik and Shabanov, Hunter, Fox and Hunter, and Campos, Fox and Schildkraut, and says its bound gives the full superexponential limit and holds uniformly down to two colors, where Fox and Hunter's needs three colors and Campos, Fox and Schildkraut's settles only $W_2(k)/2^k$. The manuscript has a library card, with the main theorem on its Theorem 1.1 page. The release's README says its manuscripts were produced by an internal OpenAI model and that the collection includes results at different stages of verification.

The bearing on Problem 176 is through the identity $N(k,k)=W(k)$, which the site's commentary on the problem states and the manuscript does not. A $k$-term progression carries $k$ signs, so its sum has absolute value at most $k$ and the parity of $k$; a sum of absolute value at least $k-1$ is therefore a sum of absolute value exactly $k$, a monochromatic progression, so $N(k,k-1)=W(k)$ as well (the case $\ell=k-1$ of a parity remark in the site's thread, recorded on the problem page). Hence the manuscript's theorem gives $N(k,k)>k^{k/100000}$ for all large $k$, which no exponential $C^k$ bounds. The first displayed question of the Statement therefore fails at $c=1$, provided the theorem holds.

Covers. The case $c=1$ of the first displayed question, whether for every $c>0$ some $C>1$ bounds $N(k,ck)$ by $C^k$, which fails because $N(k,k)=W(k)$ grows faster than any exponential. Nothing is settled for $0<c<1$, the substantive range of the question, nor for the two displayed special cases $N(k,2)$ and $N(k,\sqrt k)$, nor for the request for good upper bounds. For $c>1$ no $N(k,ck)$ exists at all, since no $k$-term sum exceeds $k$ in absolute value; that is a formulation note on the problem page, not part of this claim.

Depends on. OpenAI's accepted claim on Problem 138 supplies Theorem 1.1, the bound $W(k)>k^{k/100000}$ for all large $k$; the reduction to $N(k,k)$ is the elementary identity stated above.

Formalization. The release's Lean tree at the pinned revision states the theorem in ComparatorChallenges/QuantitativeVanDerWaerden.lean (OAI.QuantitativeVanDerWaerden.uniform_lower_bound: for some $K$, every $k\ge K$ and $r\ge2$ have $k^{k\lfloor\log_2r\rfloor/100000}<W(r,k)$ over the reals, with W r k the least positive $N$ such that every coloring $\mathbb N\to\mathrm{Fin}\,r$ has a one-color $k$-term progression with positive step inside $[0,N)$), with sorry as the challenge form, and proves it in OAI/Combinatorics/ProgressionColoring/Main.lean, which also derives kthRoot_tendsto (the divergence of $W(r,k)^{1/k}$ for each $r\ge2$). The comparator record permits only propext, Quot.sound and Classical.choice; the release's catalog formalization.yaml lists the declaration; toolchain leanprover/lean4:v4.34.1. For Problem 138 this corpus's verification built uniform_lower_bound and kthRoot_tendsto at the pinned revision and checked that their axioms are exactly propext, Classical.choice and Quot.sound, with the comparator fingerprint identical; that record is Problem 138's. Nothing about $N(k,\ell)$ or the identity above was formalized or reviewed, so formalized is not listed as evidence here.

Standing. Claimed, partial. The manuscript is a release preprint with no journal record and no independent review known to this corpus; the site's page for Problem 176 was OPEN last edited 4 April 2026, with no proof claim and thirteen comments, all earlier than the release; they include the Lean bounds for $N(k,2)$ and $N(k,\sqrt k)$ recorded on their own pages, and none settles the case $c=1$. A refereed version, a documented independent acceptance, or a kernel-checked formalization of the reduction to this problem whose statement this corpus audits would be needed before anything here moves to accepted.