---

Claim. The preprint Quasipolynomial bounds for arithmetic progressions of the OpenAI mathematics release (dated 23 September 2026, authored by OpenAI) states as its Theorem 1.1 that for each fixed integer $k\ge3$ there are constants $C_k,c_k,\varepsilon_k>0$ such that for every $N\ge2$

$$r_k(N)\le C_kN\exp\bigl(-c_k(\log N)^{\varepsilon_k}\bigr),$$

where $r_k(N)$ is the largest size of a subset of $\{1,\ldots,N\}$ with no $k$-term progression of positive common difference; equivalently, a subset of $\{1,\ldots,N\}$ of density $\alpha$ contains such a progression once $\log N$ exceeds a fixed power of $2+\log(1/\alpha)$. The manuscript's intake card is openai_2026_quasipolynomial_bounds_arithmetic_progressions. The manuscript's target is Erdős's reciprocal-sum conjecture, Problem 3, which its Corollary 1.2 derives by summing the bound over dyadic intervals; it also derives a divergence criterion with logarithmic weights and recovers the Green–Tao theorem on the primes. For Problem 139 the bound gives $r_k(N)=o(N)$ directly, since the exponential factor tends to zero, with the cases $k\le2$ trivial. The problem is already proved by Szemerédi (claim page); this is a second route whose bound is stronger than those the problem page records for every $k\ge4$ (the manuscript claims no improvement of the three-term exponent, where Kelley and Meka's bound has the same shape), by a density-increment argument over polynomial cells whose logarithmic losses the manuscript keeps polynomial in $\log(1/\alpha)$.

Depends on. Nothing in this wiki; the theorem is the manuscript's own.

Formalization. The release's Lean tree at the pinned revision defines, in OAI/Combinatorics/Progressions/Model.lean, OAI.Erdos3.extremalNumber k N as the largest size of a subset of $\{1,\ldots,N\}$ free of $k$-term progressions with positive difference, which is exactly $r_k(N)$, and QuantitativeDensityBound k as the existence of $C,c,\eta>0$ with

$$r_k(N)\le CN\exp\bigl(-c(\log\log N)^{1+\eta}\bigr) \quad\text{for every }N\ge3;$$

QuantitativeDensityTheorem asserts this for every $k\ge3$, and OAI/Combinatorics/Progressions/Results/Conclusions.lean proves it as OAI.Erdos3.manuscriptQuantitativeDensityTheorem, the first component of manuscript_main_theorems. The formalized saving, a power of $\log\log N$ above one, is weaker than the manuscript's power of $\log N$, but it still gives $r_k(N)=o(N)$ for every $k\ge3$. The second component, manuscriptReciprocalProgressionTheorem, is the statement pinned by the comparator challenge ComparatorChallenges/ErdosReciprocal.lean, whose record permits only propext, Quot.sound and Classical.choice; the release's own description of the family says the quantitative bound lies outside the pinned statement, and no comparator challenge pins the quantitative declaration. Toolchain leanprover/lean4:v4.34.1.

Acceptance. Formalized. This corpus's verification built OAI.Erdos3.manuscriptQuantitativeDensityTheorem at the pinned revision with the toolchain leanprover/lean4:v4.34.1 and checked its axioms, which are exactly propext, Classical.choice and Quot.sound. No comparator challenge pins the declaration, so it has no fingerprint to match; its statement and the definitions it uses were audited against the problem instead. extremalNumber k N is exactly $r_k(N)$, since HasAP asks for a positive common difference; the hypothesis $N\ge3$ keeps $\log\log N$ positive, so the real power takes no junk value; and the exponential factor tends to zero, so the bound gives $r_k(N)=o(N)$ for every $k\ge3$, while for $k\le2$ the claim is trivial because $r_k(N)\le1$. The pinned manuscriptReciprocalProgressionTheorem is not this page's route: it implies $r_k(N)=o(N)$ only through the classical argument that Erdős's reciprocal-sum conjecture implies Szemerédi's theorem, which is not formalized. The acceptance is of the Lean statement so audited, a second route to a problem already proved by Szemerédi. Not reviewed and not refereed: the manuscript is a release preprint with no journal record and no outside review recorded, so its Theorem 1.1, whose saving is stronger than the formalized one, stays unreviewed; the release's README says its manuscripts were produced by an internal OpenAI model and that its results are at different stages of verification. On 2026-09-04 the site's page for Problem 139 showed PROVED (LEAN) with no mention of the release.