Oct 6, 2026
Lean formalization in OpenAI math repository (Result 160)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Quantitative Superexponential Bounds for van der Waerden Numbers'. We prove that there are absolute constants c > 0 and K0 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 160). The Lean development was not rebuilt locally.