Erdős Problem #138

Read our full write-up →

Erdős offered $500 for a proof or disproof that the two-colour van der Waerden number satisfies W(k)^(1/k) → ∞; the page's best lower bound was exponential — Kozik–Shabanov's c·2^k, and since August Campos–Fox–Schildkraut's k·2^(k−1), which settles the weaker W(k)/2^k question and not this one. OpenAI's 23 September 2026 paper proves W_r(k) > k^(ck⌊log₂ r⌋) with c = 10⁻⁵ for every r ≥ 2 and all k past one absolute threshold: a two-colouring of a cyclic group of size k^(ck) built from an outer local-lemma colouring of coordinate labels, a balanced-or-globally-affine dichotomy driven by a dilation that makes every short rational period vanish, and a sparse Bernoulli perturbation keyed on Behrend-type norm bands, then a digit product for every number of colours. Its catalogued Lean (115 modules) compiled on our machine in 430 s; under --trust=0 the kernel printed only propext, Classical.choice and Quot.sound on the theorem, on kthRoot_tendsto — the page's sentence at r = 2 — and on the cyclic witness; the statement and its four definitions are byte-identical to the comparator; a wrong-shape control is rejected and a planted sorry reports sorryAx. Seven tool-equipped seats, each briefed to refute, read the paper's own TeX line by line and found no gap in the proof of Theorem 1.1 — only that the Lean proves the §3 and §6 counts in weaker forms than the paper prints, that the key-multiplicity bound is really 2, and that the sizes are astronomical: the bound beats 2^k only past k ≈ 10^30103 and the threshold sits near 10^45. The question is answered yes; the improve-the-bounds half of the page stays open. The theorem is OpenAI's; the audit and the replay are ours.