Superexponential growth of van der Waerden numbers
From OpenAI Aftermath
Superexponential growth of van der Waerden numbers concerns the van der Waerden number Wr(k), the least N such that every coloring of {1, …, N} with r colors contains a monochromatic k-term arithmetic progression. Erdős asked whether W(k)1/k tends to infinity in the two-color case. A manuscript dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims the lower bound Wr(k) > kck⌊log2 r⌋ with an absolute c > 0, uniformly in r ≥ 2, which answers this question. The collection includes a Lean formalization of this statement. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- Early lower bounds are due to Erdős and Rado and to Schmidt. Berlekamp's algebraic construction gives W2(p + 1) > p2p for primes p, Szabó proved W2(k) ≥ 2k/kε for large k, Kozik and Shabanov obtained Wr(k) ≥ βrk−1 for all r ≥ 2 and k ≥ 3, and Hunter improved the exponential base for each fixed r ≥ 5.
- Fox and Hunter proved W3(k) > 2k log*k/4 for large k, and a bound of the form r(1−ε)k log k when r is large in terms of k. Campos, Fox and Schildkraut proved W2(k) ≥ (1 − o(1))k2k−1, settling whether W2(k)/2k tends to infinity; the manuscript notes that they credit ChatGPT 5.6 Sol Pro with the coloring and an initial proof.
The original result
- Claim. Theorem 1.1 of Quantitative Superexponential Bounds for van der Waerden Numbers states that there is an absolute integer K0 such that Wr(k) > kck⌊log2 r⌋ with c = 10−5 for every k ≥ K0 and every r ≥ 2. In particular Wr(k)1/k tends to infinity for each fixed r ≥ 2, which the manuscript describes as a quantitative positive resolution of Erdős's question, including the two-color case.
- Method, as described: a two-coloring of a cyclic group of prime-power order built from two systems of circle coordinates, one of them dilated by an integer that absorbs the primary parts of all short periods; an outer coloring of the coordinate labels arranged so that every k-term progression either contains a positive proportion of each outer color or has affine real representatives; and independent rare random flips attached to keys formed by a coordinate box and an integer squared-norm band, controlled by a finite local lemma. The key quantitative input is a count of patterns through one label with a constant independent of the dimension. A digit product passes to all r ≥ 2.
- Sources. The manuscript Quantitative Superexponential Bounds for van der Waerden Numbers at commit
1581d4c. - Formalization, as described by the repository. The scope note states that the formalized result gives an absolute threshold K such that W(r, k) > kk⌊log2 r⌋/100000 for all k ≥ K and r ≥ 2, and establishes the associated growth limits, finiteness and boundary values; the sharper intermediate estimates used in the paper are not part of the described formalization. The Comparator statement is
QuantitativeVanDerWaerden.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 20 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full". Its review note states that the headline theorem carries c = 10−5 and the uniformity in r, that the strict inequality also forces finiteness because the number is defined as an infimum, and that the limit statement is the routine corollary, not stated separately. It records a sandboxed Comparator pass. | MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-09 | rohanarun/van-der-waerden-refinement (GitHub) | Extension (conditional) | Proposes conditional parameter-transfer arguments that enlarge the coefficient c with a threshold independent of r. They start from an elementary lemma that at most two points of one key occur, where the manuscript uses four. Earlier versions of the README admitted smaller coefficients such as 1/200 and 1/19; the current one states c = 1/9. The repository also discusses selected matrix-multiplication profile inequalities from another manuscript of the collection. | The README describes the work as AI-generated with Codex, with parts prepared with Claude and with a ChatGPT Pro response, conditional on stated upstream inputs, and without independent human review or formal verification. An open pull request adds conditional proof reviews and selected Lean proofs with imported assumptions, which the README says do not constitute end-to-end formal verification. |
| 2026-10-10 | cert-machine, openai/math lane K: run 38019899278 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the QuantitativeVanDerWaerden solution, in 254 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list QuantitativeVanDerWaerden, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-11 | Google DeepMind Formal Conjectures, Erdős Problem 138 (commit 3dfd999, pull request #6898) |
Catalogue (formal statement status) | States Erdős's question whether W(k)1/k tends to infinity, marks it as solved, cites the manuscript, and links the collection's Lean proof as its formal proof. | Merged into the repository. |
| 2026-10-14 | rohanarun/openai-math-illustrated (GitHub) | Reading (exposition) | An illustrated reading edition: a nine-page guide with worked examples and diagrams of the construction, followed by the original manuscript pages. | The repository describes itself as independent reading editions of the collection's manuscripts. |
| 2026-10-16 | Erdős Problem #138 on erdosproblems.com (page as last edited 16 October 2026) | Catalogue (problem page) | The page states that a formal proof that Wr(k) ≥ kck log r for all r ≥ 2, for some constant c > 0, is available, linking the collection's Lean statement. | Problem database. Its summary of bounds still names Kozik and Shabanov's W(k) ≫ 2k as the best general lower bound. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
