View source for Superexponential growth of van der Waerden numbers

'''Superexponential growth of van der Waerden numbers''' concerns the van der Waerden number ''W''<sub>''r''</sub>(''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'')<sup>1/''k''</sup> tends to infinity in the two-color case. A manuscript dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]) claims the lower bound ''W''<sub>''r''</sub>(''k'') &gt; ''k''<sup>''ck''⌊log<sub>2</sub> ''r''⌋</sup> with an absolute ''c'' &gt; 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 ''W''<sub>2</sub>(''p'' + 1) &gt; ''p''2<sup>''p''</sup> for primes ''p'', Szabó proved ''W''<sub>2</sub>(''k'') ≥ 2<sup>''k''</sup>/''k''<sup>''ε''</sup> for large ''k'', Kozik and Shabanov obtained ''W''<sub>''r''</sub>(''k'') ≥ ''βr''<sup>''k''&minus;1</sup> for all ''r'' ≥ 2 and ''k'' ≥ 3, and Hunter improved the exponential base for each fixed ''r'' ≥ 5.
** Fox and Hunter proved ''W''<sub>3</sub>(''k'') &gt; 2<sup>''k'' log<sup>*</sup>''k''/4</sup> for large ''k'', and a bound of the form ''r''<sup>(1&minus;''ε'')''k'' log ''k''</sup> when ''r'' is large in terms of ''k''. Campos, Fox and Schildkraut proved ''W''<sub>2</sub>(''k'') ≥ (1 &minus; o(1))''k''2<sup>''k''&minus;1</sup>, settling whether ''W''<sub>2</sub>(''k'')/2<sup>''k''</sup> 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 ''K''<sub>0</sub> such that ''W''<sub>''r''</sub>(''k'') &gt; ''k''<sup>''ck''⌊log<sub>2</sub> ''r''⌋</sup> with ''c'' = 10<sup>&minus;5</sup> for every ''k'' ≥ ''K''<sub>0</sub> and every ''r'' ≥ 2. In particular ''W''<sub>''r''</sub>(''k'')<sup>1/''k''</sup> 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 [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Quantitative-Superexponential-Bounds-for-van-der-Waerden-Numbers-September-23-2026 Quantitative Superexponential Bounds for van der Waerden Numbers] at commit <code>1581d4c</code>.
* '''Formalization, as described by the repository.''' The [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/160.md scope note] states that the formalized result gives an absolute threshold ''K'' such that ''W''(''r'', ''k'') &gt; ''k''<sup>''k''⌊log<sub>2</sub> ''r''⌋/100000</sup> 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 <code>QuantitativeVanDerWaerden.lean</code>.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 20 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) || Review (fidelity of the formal statements) || Rates this family "full". Its review note states that the headline theorem carries ''c'' = 10<sup>&minus;5</sup> 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 || [https://github.com/rohanarun/van-der-waerden-refinement/tree/63bef9ca996786a41169de4a0c3d6b3b47b0fe96 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 [https://github.com/rohanarun/van-der-waerden-refinement/pull/10 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: [https://github.com/carlostoledo1891/cert-machine/blob/d93dd5b48e798372da73a42ac2275a3eeacd9a5e/corpus/openai-math/kernel-runs/38019899278/QuantitativeVanDerWaerden.json run 38019899278] || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept the <code>QuantitativeVanDerWaerden</code> 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 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, memory, errors) does not list <code>QuantitativeVanDerWaerden</code>, so it was accepted by con-leche and by Lean's official kernel. || Development journal.
|-
| 2026-10-11 || Google DeepMind [https://github.com/google-deepmind/formal-conjectures Formal Conjectures], [https://github.com/google-deepmind/formal-conjectures/blob/3dfd999dfe5a3a1c739d362d3189daf9e08d9fa8/FormalConjectures/ErdosProblems/138.lean Erdős Problem 138] (commit <code>3dfd999</code>, pull request #6898) || Catalogue (formal statement status) || States Erdős's question whether ''W''(''k'')<sup>1/''k''</sup> 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 || [https://github.com/rohanarun/openai-math-illustrated/tree/80375f4b6a7aa27d6428ea505026734154fb400e/papers/van-der-waerden 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 || [https://www.erdosproblems.com/138 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 ''W''<sub>''r''</sub>(''k'') ≥ ''k''<sup>''ck'' log ''r''</sup> for all ''r'' ≥ 2, for some constant ''c'' &gt; 0, is available, linking the collection's Lean statement. || Problem database. Its summary of bounds still names Kozik and Shabanov's ''W''(''k'') ≫ 2<sup>''k''</sup> 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.

[[Category:OpenAI results]]