The claim. The answer to Problem 3 is yes: every $A\subseteq\mathbb N$ with $\sum_{n\in A}1/n=\infty$ contains arithmetic progressions of every finite length. The claimed result is Corollary 1.2 of 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 corollary is paged at Corollary 1.2. The corollary is deduced from the manuscript's Theorem 1.1 (paged at Theorem 1.1): for each 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 $k$-term arithmetic progression of positive common difference. The deduction is the one the site's commentary anticipates: a set with no $k$-term progression meets each dyadic interval $[2^m,2^{m+1})$ in at most $r_k(2^m)$ elements, so its reciprocal sum is at most $1+\sum_{m\ge1}2^{-m}r_k(2^m)$, which the bound makes finite; lengths one and two follow from the infinitude of a set with divergent reciprocal sum. The manuscript's Corollary 11.2 (paged at Corollary 11.2) states the quantitative form, a bound $H_k$ on the reciprocal sum of every $k$-term-progression-free set, and Section 11 extends the criterion to the weights $(\log(2+a))^B/a$ for every fixed $B\ge0$ and recovers the theorem of Green and Tao on dense subsets of the primes. This page covers the introduction and Section 11; the proof of Theorem 1.1 (Sections 2--10, a density increment over polynomial cells whose total logarithmic loss stays polynomial in $\log(1/\alpha)$) is outside its account. The manuscript claims no improvement of the three-term exponent, where the bounds of Kelley and Meka and their successors already have the summable shape.

The formalization. The release's Lean tree at the pinned revision proves

theorem manuscriptReciprocalProgressionTheorem : ReciprocalProgressionTheorem

as OAI.Erdos3.manuscriptReciprocalProgressionTheorem in lean/OAI/Combinatorics/Progressions/Results/Conclusions.lean, the second component of manuscript_main_theorems. Here ReciprocalProgressionTheorem is the proposition that every A : Set ℕ with ¬ Summable (reciprocalTerm A) satisfies HasAP A k for every k : ℕ; reciprocalTerm A n is $n^{-1}$ for n ∈ A and $0$ otherwise, 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 restates the three definitions it depends on, identical to the model file, so the compared statement includes them, 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 of Theorem 1.1. The statement agrees with the site's question: Lean's ℕ admits $0\in A$, whose term is Lean's junk value $0^{-1}=0$ and adds nothing to the sum; the terms are nonnegative, so non-summability is the divergence of the partial sums; and a progression with positive common difference has distinct terms.

Depends on. No page of this wiki. The three-term case of Bloom and Sisask, which has its own claim page beside this one, and the theorem of Green and Tao cited on the problem page are prior work the manuscript cites and recovers, not proof inputs.

Acceptance. Formalized. This corpus's verification built OAI.Erdos3.manuscriptReciprocalProgressionTheorem at the pinned revision and checked its axioms, which are exactly propext, Classical.choice and Quot.sound; the comparator challenge lean/ComparatorChallenges/ErdosReciprocal.lean pins the declaration with its three definitions, and its fingerprint was found identical to the challenge. Not reviewed: the manuscript is a release preprint with no journal record, no arXiv version and no outside review located, and the release's own README says that its manuscripts were produced by an internal OpenAI model and are at different stages of verification. The site's page for Problem 3, accessed 2026-10-06, shows OPEN, no proof claim and no mention of the release in its commentary (page last edited 4 April 2026). The same manuscript's Theorem 1.1 bears on Problem 142 as an improved upper bound, and gives second routes to Problem 139 and Problem 219, each recorded on its own claim page.