Superexponential van der Waerden numbers

1 paperLean

Resolves Erdős's superexponential-growth question for van der Waerden numbers. If \(W_r(k)\) is the least interval length forcing a monochromatic k-term progression in every r-coloring, then \(W_r(k)\gt k^{ck\lfloor\log_2 r\rfloor}\) for an absolute c > 0, all r ≥ 2 and sufficiently large k, uniformly in r. In particular, \(W_r(k)^{1/k}\to\infty\) for each fixed r.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

Quantitative Superexponential Bounds for van der Waerden Numbers

OpenAI · September 23, 2026

We prove that there are absolute constants c > 0 and K₀ such that \(W_r(k)\gt k^{ck\lfloor\log_2 r\rfloor}\) for every \(k\ge K_0\) and r ≥ 2. Consequently \(W_r(k)^{1/k}\to\infty\) for each fixed r ≥ 2, giving a quantitative positive resolution of Erdős's superexponential-growth question, including the two-color case.

Read PDF Download Source

Cite

@misc{OAI:Quantitative-Superexponential-Bounds-for-van-der-Waerden-Numbers-September-23-2026,
  author = {{OpenAI}},
  title = {{Quantitative Superexponential Bounds for van der Waerden Numbers}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Quantitative-Superexponential-Bounds-for-van-der-Waerden-Numbers-September-23-2026/paper.pdf}{OAI:Quantitative-Superexponential-Bounds-for-van-der-Waerden-Numbers-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Quantitative Superexponential Bounds for van der Waerden Numbers

Scope

Let \(W(r,k)\) be the least interval length forcing a monochromatic \(k\)-term arithmetic progression in every coloring with at most \(r\) colors. The formalized result gives an absolute threshold \(K\) such that \(W(r,k)>k^{k\lfloor\log_2 r\rfloor/100000}\) for all \(k\ge K\) and \(r\ge2\). It also establishes the associated growth limits, finiteness, and boundary values. The sharper intermediate estimates used in the paper are not part of the described formalization.

Comparator links

Result	Comparator statement
Uniform van der Waerden lower bound	QuantitativeVanDerWaerden.lean

Scope note on GitHub →