Quasipolynomial Bounds for Arithmetic Progressions

Comments and discussion

• Thomas Bloom, Erdős problems in the OpenAI proofs, with comment thread (MalekZ, jleng01, Thomas Bloom) (erdosproblems.com blog and forum, 8–12 Oct 2026). Bloom summarizes the claimed bound for all k ≥ 3, notes that a bound of this shape was already known for k=3 (Kelley–Meka), and says the Lean code "appears to prove the weaker bound" exp(-(log log N)^{1+c_k})N. In the comments, jleng01 calls the proof "largely a synthesis of previous work on the problem," and Bloom agrees that it shows existing techniques "pushed sufficiently far" suffice.

Formalization

• OpenAI, Erdős’s reciprocal-sum conjecture and quasipolynomial Szemerédi bounds: Lean scope notes (lean/docs/159.md, 6 October 2026). States that the formalization proves the reciprocal-sum corollary (progressions of every length with positive common difference), with a proof declaration in Conclusions.lean, and that the quantitative bound on r_k(N) is outside the formal statement. [family-level]
• OpenAI, ErdosReciprocal.lean Comparator challenge (openai/math, commit adc7f12). Defines ReciprocalProgressionTheorem (a non-summable reciprocal sum implies HasAP A k for all k). The proof in the challenge file is left as sorry by design, to be supplied by the solution module.
• google-deepmind/formal-conjectures, ErdosProblems/3.lean (formal-conjectures). Marks erdos_3 as research solved, cites this paper as [OAI26] and links the OpenAI Lean proof; also states Kelley–Meka, Bloom–Sisask, Green–Tao, Gowers and Leng–Sah–Sawhney bounds as variants.
• MathVet, fidelity-table.csv (row 159) (mathvet/mathvet, Oct 2026). Records coverage as "partial" and a comparator pass for ErdosReciprocal, noting that the quantitative Szemerédi bound is not stated.
• Neal McBurnett, openai-math-lean-tooling configs.csv (run started 10 Oct 2026). Independent Comparator re-run with ErdosReciprocal status "accepted" (solution module OAI.Combinatorics.Progressions.Main, about 2472 s check time, 14.3 GiB peak RSS).
• plasma-ai, E0003 claim page: 2026_09_23_openai (plasma-ai/erdos wiki, 7 Oct 2026). Records Corollary 1.2 as accepted after building OAI.Erdos3.manuscriptReciprocalProgressionTheorem and checking that it uses only standard axioms; states that Theorem 1.1's proof is not covered.

Related prior literature mentioned by others

• Thomas F. Bloom and Olof Sisask, Breaking the logarithmic barrier in Roth’s theorem on arithmetic progressions (arXiv:2007.03528, 7 July 2020; revised 1 September 2021). Kalai’s October 2026 post identifies this three-term reciprocal-sum result as the predecessor to the manuscript’s claimed extension to every finite progression length.

Possibly relevant literature (found by the agent, not checked)

• Sarah Peluse, Finding arithmetic progressions in dense sets of integers (arXiv:2509.22962, Sept 2025). Survey of recent higher-order Fourier progress behind the k ≥ 5 bounds that the introduction's prior-bounds discussion builds on.
• Joni Teräväinen and Mengdi Wang, On the Green-Tao theorem for sparse sets (arXiv:2603.09281, Mar 2026). Proves a quantitative relative-density bound exp(-(log log log N)^{c_k}) for k-AP-free subsets of the primes, which bears on the paper's claim that it recovers the Green–Tao relative-density theorem.

Digests and expositions

• Azmat, Erdős–Turán Conjecture: How OpenAI Tackled the Arithmetic Progression Barrier (BinaryVerse AI, 11 October 2026). Outlines the manuscript’s density-increment argument using triangular polynomial cells and distinguishes its quantitative bound, reciprocal-sum consequence, and published Lean scope.
• Ying Xie, What the Machine Invented: Mining New Mathematical Instruments from OpenAI's October 2026 Release of AI-Generated Mathematics (arXiv:2610.17090, 12 Oct 2026). Has a family card for 159 (Section 8.3.5) and labels the triangular polynomial cells with precision budgets as a "new architecture"; it calls its novelty verdicts provisional. [family-level]

News and blogs

• José Hdz. Stgo., The long-awaited simple proof of the Green-Tao theorem is finally here! (Apuntes misceláneos, 7 October 2026). Observes that the manuscript’s Corollary 1.2, together with divergence of the sum of reciprocals of primes, implies arbitrarily long arithmetic progressions in the primes.