---

Claim. Problem 140 is proved by a second route. Theorem 1.1 of OpenAI, Quasipolynomial Bounds for Arithmetic Progressions (release preprint dated 23 September 2026, the claim's date; family 159 of the release; its intake card is openai_2026_quasipolynomial_bounds_arithmetic_progressions), asserts that for each fixed integer $k\ge3$ there are constants $C_k,c_k,\varepsilon_k>0$ with

$$r_k(N)\le C_k\,N\exp\bigl(-c_k(\log N)^{\varepsilon_k}\bigr) \qquad\text{for every }N\ge2,$$

where $r_k(N)$ is the largest size of a subset of $\{1,\ldots,N\}$ with no $k$-term progression of positive common difference. At $k=3$ the factor $\exp(-c_3(\log N)^{\varepsilon_3})$ is eventually below $(\log N)^{-C}$ for every fixed $C>0$, so $r_3(N)\ll N/(\log N)^C$, the site's statement. For each fixed $k\ge4$ the same theorem gives $r_k(N)\ll_{k,C}N/(\log N)^C$ for every $C>0$. This is the extension to every $k$ that the site's commentary records as conjectured in [ErGr80] and [Er81]. No earlier result proves it for any $k\ge4$: the best earlier bounds are Green and Tao's $N/(\log N)^c$ for one small $c>0$ at $k=4$ and Leng, Sah and Sawhney's $N\exp(-(\log\log N)^{c_k})$ for $k\ge5$. The paper's stated contribution is the all-length bound and its consequence Corollary 1.2, Erdős's reciprocal-sum conjecture (Problem 3); its introduction (pp. 5--6) records the stronger three-term bound of Kelley and Meka and says that no improvement of the three-term exponent is claimed. The statement and Corollary 1.2 are on pp. 4--5 of the release PDF, and the card's result page Theorem 1.1 records the statement; this corpus has not reviewed the proof (about 190 pages).

Formal statement. The release's lean/ folder, at the pinned commit, proves OAI.Erdos3.manuscriptQuantitativeDensityTheorem (OAI/Combinatorics/Progressions/Results/Conclusions.lean): for every $k\ge3$ there are reals $C,c,\eta>0$ with $\mathrm{extremalNumber}\,k\,N\le C\,N\exp(-c(\log\log N)^{1+\eta})$ for every $N\ge3$, where extremalNumber k N (Model.lean) is the largest cardinality of a subset of Finset.Icc 1 N with no $k$-term progression of positive difference, that is, $r_k(N)$. This Lean bound is weaker than the paper's Theorem 1.1 (a power of $\log\log N$ in the exponent, not of $\log N$). The library lemma OAI.Erdos3.QuantitativeDensityBound.logarithmic (Estimates/UniformRelativePatchSource.lean) turns the bound for one $k$ into: for every real $B>0$ there is $C>0$ with $\mathrm{extremalNumber}\,k\,N\le C\,N/(\log N)^B$ for every $N\ge3$. Applying it to the theorem at $k=3$ gives exactly the problem's statement, and at any $k\ge3$ the every-$k$ extension; that one-line combination is not a declaration of the release and is stated here. The release's comparator challenge ComparatorChallenges/ErdosReciprocal.lean pins only manuscriptReciprocalProgressionTheorem, the reciprocal-sum consequence, which does not by itself imply the problem's statement (a bound of order $N/(\log N)^{3/2}$ would satisfy it and fail the problem at $C=2$); manuscriptQuantitativeDensityTheorem is the first component of manuscript_main_theorems, whose second component is the pinned manuscriptReciprocalProgressionTheorem, and no challenge pins it or the lemma QuantitativeDensityBound.logarithmic, which takes the bound as a hypothesis. The release's scope note for the family (lean/docs/159.md) says the quantitative bound is outside the formalized statement it selected.

Depends on. Nothing in this wiki: the route is independent of Kelley and Meka's accepted proof on its claim page.

Acceptance. Formalized. This corpus's verification built OAI.Erdos3.manuscriptQuantitativeDensityTheorem and OAI.Erdos3.QuantitativeDensityBound.logarithmic at the pinned revision with the toolchain leanprover/lean4:v4.34.1 and checked their axioms, which for each are exactly propext, Classical.choice and Quot.sound. No comparator challenge pins either declaration, so neither has a fingerprint to match; their statements were audited against the problem instead. extremalNumber 3 N is exactly $r_3(N)$; the theorem at $k=3$ bounds it by $C\,N\exp(-c(\log\log N)^{1+\eta})$ for every $N\ge3$, and the lemma turns that bound into $r_3(N)\le C\,N/(\log N)^B$ for every real $B>0$ and every $N\ge3$, which is the problem's statement. Combining the two is the one-line step stated under Formal statement., not a declaration of the release. The same combination at each $k\ge4$ gives $r_k(N)\ll_{k,B}N/(\log N)^B$, the extension the site's commentary records as conjectured, which lies outside the problem's statement. The pinned manuscriptReciprocalProgressionTheorem gives this page no support: it forces only $\sum_m2^{-m}r_3(2^m)<\infty$, which a bound of order $N/(\log N)^{3/2}$ would satisfy. The acceptance is of the Lean statements so audited, a second route to a problem already proved through Kelley and Meka, so this page changes no standing. Not reviewed and not refereed: the preprint has no journal record, arXiv version or published independent review, so its Theorem 1.1, whose saving is stronger than the formalized one, and its roughly 190-page proof stay 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, and the site's page carried no comment or proof-claim entry on 2026-10-07.