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 consequence is paged at Corollary 1.2), states in its Theorem 1.1 that for every fixed $k\ge3$ there are constants $C_k,c_k,\varepsilon_k>0$ with

where $r_k(N)$ is the largest size of a subset of $\{1,\dots,N\}$ with no nonconstant $k$-term arithmetic progression, and deduces as Corollary 1.2, by summing the bound over dyadic intervals, that every set $A\subseteq\mathbb N$ with $\sum_{a\in A}1/a=\infty$ contains nonconstant arithmetic progressions of every finite length. The manuscript answers Erdős's reciprocal-sum conjecture, which this wiki records as Problem 3. Its Section 11.3, in the unnumbered paragraph "Dense subsets of the primes", claims to recover from Theorem 1.1 the theorem of Green and Tao that every subset of the primes of positive relative upper density contains infinitely many $k$-term progressions for every $k$; with the whole set of primes that claim would answer Problem 219 yes directly, a second route beside the theorem of Green and Tao. Corollary 1.2 applied to the primes gives the same answer through the divergence of $\sum1/p$, which the manuscript does not reprove; that route, not the dense-primes paragraph, is the one the Lean declaration below supports. The release states that its manuscripts were produced by an internal OpenAI model and come at different stages of verification, not all with Lean formalizations.

The formalization. The release's Lean tree at the pinned revision (Lean v4.34.1, Mathlib at the revision the release's manifest pins) proves

theorem manuscriptReciprocalProgressionTheorem : ReciprocalProgressionTheorem

as OAI.Erdos3.manuscriptReciprocalProgressionTheorem in lean/OAI/Combinatorics/Progressions/Results/Conclusions.lean, where ReciprocalProgressionTheorem is the proposition that every A : Set ℕ with ¬ Summable (reciprocalTerm A) satisfies HasAP A k for every k, reciprocalTerm A n is $1/n$ on A and $0$ off it, and HasAP A k asks for a and d > 0 with a + i * d ∈ A for all i < k. The comparator challenge lean/ComparatorChallenges/ErdosReciprocal.lean, with its configuration ErdosReciprocal.json, pins that declaration and carries the three definitions HasAP, reciprocalTerm and ReciprocalProgressionTheorem, and permits only the axioms propext, Quot.sound and Classical.choice; the release's page lean/docs/159.md says the formalization covers the reciprocal-sum consequence and not the quantitative bound. The specialization to the primes is not a declaration in the release: it takes the set of primes, discharges the hypothesis with Mathlib's not_summable_one_div_on_primes (the same function after rewriting $1/n$ as $n^{-1}$), and reads off a $k$-term progression of primes with positive common difference for every $k$. A reader citing the formalization for Problem 219 should name that step.

Depends on. The release's reciprocal-sum claim (Corollary 1.2, the theorem the Lean declaration proves). The theorem of Green and Tao recorded on the problem page is prior work, which the manuscript cites and claims to recover but does not use as a proof input; the divergence of $\sum1/p$ is Euler's theorem, in Mathlib.

Acceptance. Formalized. This corpus's verification built OAI.Erdos3.manuscriptReciprocalProgressionTheorem 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, with no sorry; the comparator challenge lean/ComparatorChallenges/ErdosReciprocal.lean pins the declaration with its three definitions, and its fingerprint was found identical to the challenge, as recorded on the Problem 3 claim page. Mathlib's not_summable_one_div_on_primes, in the Mathlib the release pins, was built and axiom-checked with the same three axioms; it states ¬ Summable (indicator {p | p.Prime} (fun n : ℕ ↦ (1 : ℝ) / n)), which is reciprocalTerm of the set of primes pointwise after rewriting with one_div and indicator_apply. The specialization is the one-line instantiation described above and is not a declaration in the release: with $A$ the set of primes, the theorem gives for every $k$ some $a$ and $d>0$ with $a+id$ prime for all $i<k$, so the primes contain arithmetic progressions of every length with positive common difference, which is the problem's question, and the claim is full. Not reviewed: the manuscript is a release preprint with no journal record, no arXiv version and no outside review recorded, and the release's README says that its manuscripts were produced by an internal OpenAI model and are at different stages of verification. The dense-primes paragraph of Section 11.3 is not covered: Theorem 1.1, on which it rests, is the manuscript's claim alone, and the release's Lean states only a weaker density bound, with $(\log\log N)^{1+\eta}$ in place of $(\log N)^{\varepsilon_k}$ in the exponent. The problem was already settled by the refereed theorem of Green and Tao; this claim is a second route.