The claim. Let $W_r(k)$ be the least $N$ such that every coloring of $\{1,\ldots,N\}$ with at most $r$ colors has a monochromatic $k$-term arithmetic progression, so that $W(k)=W_2(k)$ is the van der Waerden number of Problem 138. Theorem 1.1 of the manuscript Quantitative superexponential bounds for van der Waerden numbers of the OpenAI mathematics release, dated 23 September 2026 and authored by OpenAI (its intake card is openai_2026_quantitative_superexponential_bounds_van_der_waerden_numbers, with the theorem paged at Theorem 1.1), states that there is an absolute integer $K_0$ such that for every integer $k\ge K_0$ and every integer $r\ge2$

with the threshold uniform in the number of colors. At $r=2$ this is $W(k)>k^{k/100000}$ for all $k\ge K_0$, so $W(k)^{1/k}\ge k^{1/100000}$ and

the example question the problem names and the statement Erdős offered the prize for; the manuscript's Corollary 7.3 (paged at Corollary 7.3) states the limit for every fixed $r\ge2$, together with a uniform rate in $k$ and the superpolynomial growth in $r$ at fixed $k\ge3$. The proof builds a two-coloring of a cyclic group $\mathbb Z/q^D\mathbb Z$ of order at least $k^{ck}$, with $q$ a power of a prime exceeding $k$ and $D=\lceil k^{1/10}\rceil$: points are labeled by boxes in two systems of circle coordinates, one dilated by a large integer so that every short rational period either collapses or exceeds $D^2$, and an independent random flip attached to each box and squared-norm band breaks the remaining progressions, with a finite local lemma proved in the manuscript; a digit product then transfers the cyclic coloring to intervals and to every number of colors. The manuscript credits the earlier two-color records it improves, among them Berlekamp's $W(p+1)>p2^p$ for primes $p$ and the bound $W(k)\gg2^k$ of Kozik and Shabanov recorded on the problem page, and notes that its bound is stronger than $W(k)/2^k\to\infty$, the question of [Er80] it credits Campos, Fox and Schildkraut with settling first (their claim page).

Covers. The page's named example question, 'prove that W(k)^{1/k} → ∞' for the 2-colour van der Waerden number, is proved (kthRoot_tendsto at r = 2). It also gives the explicit lower bound W(k) > k^{k/100000} for every k ≥ an absolute K (uniform_lower_bound at r = 2). The open-ended request to 'improve the bounds' stays open; nothing is said about upper bounds.

Depends on. No page of this wiki. The theorem is the manuscript's own, and the Lean development is self-contained above Mathlib.

Acceptance. Formalized. The release's Lean tree at the pinned revision (Lean v4.34.1, Mathlib at the revision the release's manifest pins) defines, in lean/OAI/Combinatorics/ProgressionColoring/Model.lean, OAI.QuantitativeVanDerWaerden.W r k as the least positive $N$ such that every coloring ℕ → Fin r has a monochromatic $k$-term progression with positive common difference inside $[0,N)$, which at $r=2$ is $W(k)$ (a shift carries $\{1,\ldots,N\}$ to $[0,N)$, the property is upward closed, and an empty infimum would be $0$ and falsify the strict bound). The file lean/OAI/Combinatorics/ProgressionColoring/Main.lean proves

theorem uniform_lower_bound :
    ∃ K : ℕ, ∀ k ≥ K, ∀ r ≥ 2,
      (k : ℝ) ^ ((1 / 100000 : ℝ) * k * (Nat.log 2 r : ℝ)) < (W r k : ℝ)

theorem kthRoot_tendsto {r : ℕ} (hr : 2 ≤ r) :
    Tendsto (fun k : ℕ => (W r k : ℝ) ^ (1 / (k : ℝ))) atTop atTop

as OAI.QuantitativeVanDerWaerden.uniform_lower_bound and OAI.QuantitativeVanDerWaerden.kthRoot_tendsto; at $r=2$, where Nat.log 2 2 = 1, the first is $W(k)>k^{k/100000}$ and the second is $W(k)^{1/k}\to\infty$ literally. This corpus's verification built both declarations at the pinned revision and checked their axioms, which are exactly propext, Classical.choice and Quot.sound; the comparator challenge lean/ComparatorChallenges/QuantitativeVanDerWaerden.lean, with its configuration QuantitativeVanDerWaerden.json, pins uniform_lower_bound with definitions identical to the model file and permits only those three axioms, and its fingerprint was found identical. The release's page lean/docs/160.md says the formalization covers the uniform bound and the growth limits and not the sharper intermediate estimates. Not reviewed: the manuscript is a release preprint with no journal record, no arXiv version and no outside review is known; the release's README says its manuscripts were produced by an internal OpenAI model and that its results are at different stages of verification. The site labels the problem OPEN (page last edited 2 June 2026) and its commentary does not mention the release; the commentary records the three-color analogue of Fox and Hunter, a different result, and credits DeepMind with $W(k+1)\ge W(k)+k$, which has its own claim page.