Quantitative density theorem (v2 series): $r_k(N)\le C N\exp(-c(\log\log N)^{1+\eta})$ for every $k\ge 3$

For every integer $k\ge 3$ there are real constants $C>0$, $c>0$, $\eta>0$ such that for every natural number $N\ge 3$

where $r_k(N)$ is extremalNumber k N: the largest cardinality of a finite set $S\subseteq\{1,\dots,N\}$ that contains no $k$-term arithmetic progression $a,a+d,\dots,a+(k-1)d$ with $d>0$ (APFree S k, the negation of HasAP S k). In Lean the statement is the proposition QuantitativeDensityTheorem, which says QuantitativeDensityBound k for every $k\ge 3$; logarithms are Real.log, natural.

This is the form of OpenAI's Theorem 1.1 recorded in OpenAI's Lean as OAI.Erdos3.manuscriptQuantitativeDensityTheorem in lean/OAI/Combinatorics/Progressions/Results/Conclusions.lean; the paper states the bound as $r_k(N)\le C_k\,N\exp\!\big(-c_k\,(\log N)^{\varepsilon_k}\big)$, and the $(\log\log N)^{1+\eta}$ form displayed above is the one the Lean development proves.

Formalization note. The present theorem is the faithful v2-series regeneration of the deprecated v1 statement: it asserts the identical proposition QuantitativeDensityTheorem, defined in the v2 definitions bundle OAIE3v2B060, so the statement is reachable from the proved *_s2 development, unlike the v1-series twin whose preamble duplicates the same names from the parallel v1 split.

Source: OpenAI, Quasipolynomial Bounds for Arithmetic Progressions, September 23, 2026, github.com/openai/math, Apache License 2.0.