---

The claim. The manuscript Quasipolynomial bounds for arithmetic progressions of the OpenAI mathematics release, dated 23 September 2026 and authored by OpenAI (its intake card is openai_2026_quasipolynomial_bounds_arithmetic_progressions, and the result is paged at Corollary 11.2), states in its Theorem 1.1 that for every fixed $k\ge3$ there are constants $C_k,c_k,\varepsilon_k>0$ with

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

where $r_k(N)$ is the largest size of a subset of $\{1,\ldots,N\}$ with no nonconstant $k$-term arithmetic progression, and deduces as Corollary 11.2 (Section 11.1, p. 82) that every $A\subseteq\mathbb N$ without a nonconstant $k$-term progression satisfies

$$\sum_{a\in A}\frac1a\le H_k:=\sum_{m\ge0}2^{-m}r_k(2^m)<\infty.$$

The proof is a paragraph: a dyadic block $[2^m,2^{m+1})$ holds at most $r_k(2^m)$ elements of $A$, each with reciprocal at most $2^{-m}$, and Theorem 1.1 makes the series converge. In the notation of Problem 169 this is $f(k)\le H_k$, so $f(k)$ is finite for every $k\ge3$. The constants $C_k,c_k,\varepsilon_k$ are not explicit, so $H_k$ is a finite number with no computed value; the manuscript does not name $f(k)$, $W(k)$ or the problem. The release's README says that its manuscripts were produced by an internal OpenAI model and that its results are at different stages of verification.

Covers. The finiteness of $f(k)$ for every $k\ge3$, with the explicit form $H_k$ of a bound. Not covered: any numerical estimate of $f(k)$, which is what the problem asks for, and the displayed question whether $f(k)/\log W(k)\to\infty$. The site's commentary records Gerver's observation that the finiteness of $f(k)$ for all $k$ is equivalent to Erdős's reciprocal-sum conjecture, Problem 3, which the same manuscript settles through its Corollary 1.2, accepted in this corpus on the claim page of Problem 3 on Lean this corpus built and audited. By Gerver's equivalence the finiteness of $f(k)$ for every $k\ge3$ follows from that accepted result, and it also follows from the accepted theorem by an elementary argument: if the series $\sum_m2^{-m}r_k(2^m)$ diverged, extremal progression-free subsets of $\{1,\ldots,4^j\}$, translated into the windows $[2\cdot4^j,3\cdot4^j]$, would form a progression-free set with divergent reciprocal sum. The bound $f(k)\le H_k<\infty$ in the form this page states stays claimed, because no accepted record derives it.

Depends on. The release's r_k(N) bound on Problem 139, Theorem 1.1 of the same manuscript, from which the corollary is deduced; that page is accepted on the release's Lean bound, a weaker saving than Theorem 1.1 that still makes $H_k$ finite, but the corollary's dyadic step is not formalized and no accepted record derives it, so this page stays claimed. Gerver's lower bound $f(k)\ge(1-o(1))k\log k$ and the other results the problem page cites are prior work the manuscript neither uses nor cites for this corollary.

Formalization. The release's Lean tree at the pinned revision proves, in lean/OAI/Combinatorics/Progressions/Results/Conclusions.lean, both the reciprocal-sum theorem, the proposition that every set with divergent reciprocal sum contains progressions of every length, pinned by the comparator challenge lean/ComparatorChallenges/ErdosReciprocal.lean, and the unpinned OAI.Erdos3.manuscriptQuantitativeDensityTheorem. The latter asserts QuantitativeDensityBound k of Model.lean for every $k\ge3$: constants $C,c,\eta>0$ with $r_k(N)\le CN\exp(-c(\log\log N)^{1+\eta})$ for every $N\ge3$. That saving is weaker than Theorem 1.1's power of $\log N$, but it is enough for convergence, since the terms $2^{-m}r_k(2^m)$ are eventually below $m^{-2}$; so $f(k)\le H_k<\infty$ follows from a proved declaration through the corollary's dyadic step, which is not formalized. No declaration states Corollary 11.2 and no comparator pins the quantitative theorem; the sentence in the release's page lean/docs/159.md that the quantitative bound is outside the formalized statement refers to the pinned theorem. The corpus's verification of the release accepted no declaration for this problem, so no formalized evidence is listed.

Acceptance. None. The manuscript is a release preprint with no journal record, no arXiv version and no published independent review; the site's label is OPEN and its commentary (page last edited 4 April 2026) does not mention the release. The claim is claimed, and the problem stays open: a partial claim derives no standing.