---
id: "2026-10-06-openai-erdos-arithmetic-progressions-conjecture-claim"
url: "https://postcutoff.com/e/2026-10-06-openai-erdos-arithmetic-progressions-conjecture-claim/"
as_of: "2026-10-30T13:42:00+01:00"
date: "2026-10-06"
date_precision: day
category: science
importance: 5
confidence: medium
status: [Awaiting review]
verification: Peer-reviewed
sources: 10
editor: human editor
human_review: null
version: "2026-10-29"
---

As of: 2026-10-30 13:42 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-10-06-openai-erdos-arithmetic-progressions-conjecture-claim/

# Erdős's arithmetic-progression conjecture claimed (OpenAI, Lean)

Full title: OpenAI's math release claims Erdős's $5000 conjecture on arithmetic progressions (a divergent reciprocal sum forces progressions of every length), via quasipolynomial bounds in Szemerédi's theorem; Lean covers the qualitative statement

"Quasipolynomial Bounds for Arithmetic Progressions" (OpenAI, dated 23 Sept 2026, released 6 Oct as family 159 of github.com/openai/math, 198 pages) states: "We prove Erdős's conjecture that every set of positive integers with divergent reciprocal sum contains arithmetic progressions of every finite length", deducing it from r_k(N) ≤ C_k·N·exp(−c_k(log N)^ε_k) for every k ≥ 3. OpenAI's Lean challenge ErdosReciprocal states only the qualitative conjecture, and the community comparator run of 25–26 Oct accepted it. Thomas Bloom says the Lean code "appears to prove the weaker bound" exp(−(log log N)^(1+c_k))·N, which still implies the conjecture, and that the paper uses "essentially all of the existing techniques currently used in the area". Google DeepMind's formal-conjectures now marks Erdős problem #3 as solved, citing the OpenAI proof. No refereed or expert check has been published.

## Key facts
- Manuscript: 'Quasipolynomial Bounds for Arithmetic Progressions', author 'OpenAI', dated 23 Sept 2026, 198 pages; family 159 of the 6 Oct release. Abstract: 'We prove Erdős's conjecture that every set of positive integers with divergent reciprocal sum contains arithmetic progressions of every finite length. More quantitatively, for every fixed k ≥ 3, we show r_k(N) ≤ C_k N exp(−c_k (log N)^ε_k)', where r_k(N) is the largest size of a subset of {1,…,N} with no k-term progression
- The problem: erdosproblems.com #3, prize $5000. Erdős offered $3000 in a 1976 talk dedicated to Paul Turán and raised it to $5000 in 1996 (Wikipedia). Because the reciprocals of the primes diverge, the Green–Tao theorem is a special case. Erdős thought the conjecture the 'only way to approach' long progressions of primes (erdosproblems.com)
- State of the art before the release (erdosproblems.com #3): the three-term case of the conjecture was proved by Bloom and Sisask (2020); Kelley and Meka (2023) gave much stronger bounds for k = 3; Green and Tao proved r_4(N) ≪ N/(log N)^c; Leng, Sah and Sawhney (2024) proved r_k(N) ≪ N/exp((log log N)^c_k) for general k, far short of what the conjecture needs
- Lean (OpenAI scope note lean/docs/159.md): the formalization proves that a set with divergent reciprocal sum contains, for every requested length, a progression with positive common difference; 'The paper's quantitative upper bound for the largest progression-free subset of {1,…,N} is outside this statement.' Challenge ErdosReciprocal: 'accepted' in the oai-math-revised comparator run of 25–26 Oct (which checks the proof against the challenge statement, not the statement against the paper)
- Thomas Bloom (erdosproblems.com blog, 8 Oct): 'For k=3 a bound of this shape was already known, by Kelley and Meka [KeMe23]. For k≥4 the known bounds were much weaker.' The Lean code 'appears to prove the weaker bound of |A| ≤ exp(−(log log N)^(1+c_k))N'. The PDF 'appears to use essentially all of the existing techniques currently used in the area: density increment methods, almost-periodicity, ideas from the Kelley-Meka argument and earlier work, Gowers inverse theory', in particular the inverse results behind the Leng–Sah–Sawhney bounds. He stresses he had 'not yet looked at in any serious way any of the proofs'
- Forum thread under Bloom's post: a commenter posting as jleng01, who says he spent 'an extensive amount of time working on the problem', wrote (9 Oct) that 'the only value of the 200 pages of AI slop is that another AI can "understand" it and explain it to a human', and (12 Oct) 'My understanding is that the proof is largely a synthesis of previous work on the problem.' Bloom replied: 'The AI proof of [3] is definitely interesting because it tells us (a) the statement is true and (b) some combination of existing techniques, pushed sufficiently far, is capable of proving it', and said he would rather look for a much simpler proof than study the AI's version
- formal-conjectures (Google DeepMind): erdos_3 is tagged 'research solved', with the docstring 'Yes. This was proved by an internal OpenAI model in September 2026 [OAI26]; see the linked Lean proof', linking OpenAI's Lean file. erdosproblems.com #3 (edited 16 Oct) says 'A formalised proof of the original conjecture of Erdős is available here' and that a companion PDF claims the stronger bound
- Other reactions: Scientific American (8 Oct) counted 'a proof of perhaps the most famous conjecture of storied problem-poser Paul Erdős' among the release's most important claims; Gil Kalai's blog (7 Oct) listed it among results connected to earlier posts; Wikipedia's article on the conjecture now records the claimed proof. OpenAI published a reasoning summary for this family (reasoning_traces/quasipolynomial-arithmetic-progressions.pdf). No dedicated Hacker News thread found

## What happened

Erdős conjectured that a set of positive integers whose reciprocals have a divergent sum must contain arithmetic progressions of every
length. He offered $3000 for it in 1976 and $5000 in 1996. The primes are such a set, so the conjecture would contain the Green–Tao
theorem. Before October 2026 it was known only for three-term progressions (Bloom and Sisask, 2020). For longer progressions the best
bounds in Szemerédi's theorem were far too weak to give it.

OpenAI's 6 Oct release includes a 198-page manuscript, dated 23 Sept, claiming quasipolynomial bounds for progression-free sets for
every length k ≥ 3. Bounds of this strength would settle the conjecture with room to spare. OpenAI's Lean formalization states and
proves only the qualitative conjecture. A community comparator run accepted it, and Google DeepMind's formal-conjectures project now
marks Erdős problem #3 as solved. Thomas Bloom, who runs erdosproblems.com, reads the formal proof as establishing a weaker
quantitative bound than the paper, still enough for the conjecture. He describes the manuscript as using essentially all existing
techniques in the area.

## Why it matters

If the statement and proof hold, the most famous of Erdős's prize problems is settled, and the formal proof makes the qualitative claim
checkable by machine. The first expert readers treat the paper less as a new method than as evidence that known tools, pushed far
enough, suffice. Bloom's response is to look for a simpler human proof rather than to digest the 198 pages. Our coverage of the release
had listed this claim only in passing.

## What is disputed or not yet verified

- Verification: Lean formalization of the qualitative statement, accepted by an independent comparator run and linked as the formal proof by formal-conjectures; the quantitative theorem is only in the unrefereed 198-page manuscript

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 159 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 98 days after its cutoff
- Gemini 4 Argon (training cutoff March 2026): 189 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 128 days after its cutoff

## Sources

1. [OpenAI (PDF): Quasipolynomial Bounds for Arithmetic Progressions (23 Sept 2026)](https://github.com/openai/math/blob/main/preprints/Quasipolynomial-Bounds-for-Arithmetic-Progressions-September-23-2026/paper.pdf) (github.com, paper)
2. [OpenAI Lean scope note for family 159](https://github.com/openai/math/blob/main/lean/docs/159.md) (github.com, code)
3. [OpenAI reasoning summary: quasipolynomial arithmetic progressions](https://github.com/openai/math/blob/main/reasoning_traces/quasipolynomial-arithmetic-progressions.pdf) (github.com, paper)
4. [erdosproblems.com: Problem #3 ($5000)](https://www.erdosproblems.com/3) (erdosproblems.com, docs)
5. [formal-conjectures: ErdosProblems/3.lean (research solved, links OpenAI's proof)](https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/3.lean) (github.com, code)
6. [oai-math-revised comparator results (ErdosReciprocal accepted)](https://github.com/mathcommunity/oai-math-revised/blob/main/checks/comparator-2026-10-26/results.tsv) (github.com, code)
7. [Wikipedia: Erdős conjecture on arithmetic progressions](https://en.wikipedia.org/wiki/Erd%C5%91s_conjecture_on_arithmetic_progressions) (en.wikipedia.org, docs)
8. [Scientific American: The most exciting claims from OpenAI's heap of new proofs (8 Oct)](https://www.scientificamerican.com/article/the-most-exciting-claims-from-openais-heap-of-new-proofs/) (scientificamerican.com, press)
9. [Thomas Bloom: Erdős problems in the OpenAI proofs (erdosproblems.com blog, 8 Oct, with comments)](https://www.erdosproblems.com/forum/thread/blog:10) (erdosproblems.com, discussion)
10. [Gil Kalai: Updates: Sharing AI progress on mathematics (amazing!) (7 Oct)](https://gilkalai.wordpress.com/2026/10/07/updates-sharing-ai-progress-on-mathematics-amazing-and-my-lecture-plans/) (gilkalai.wordpress.com, discussion)

## Changes

- 2026-10-29 (filed): Created (CONTENTS entry, PDF (198 pp), Lean scope note, comparator results, Bloom's post and forum thread, formal-conjectures, erdosproblems.com #3, Kalai, Scientific American and Wikipedia read)

## Related

- 2026-10-24: [oai-math-revised: mathematicians launch a community hub to revise OpenAI's AI-written math manuscripts (guest post on Tao's blog)](https://postcutoff.com/e/2026-10-24-oai-math-revised-community-hub/index.md)
- 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/index.md)
- 2026-10-06: [Unit-distance bound below n^(4/3) claimed (OpenAI, Lean)](https://postcutoff.com/e/2026-10-06-openai-unit-distance-upper-bound-power-saving-claim/index.md)
- People: [Timothy Gowers](https://postcutoff.com/person/timothy-gowers/), [Thomas Bloom](https://postcutoff.com/person/thomas-bloom/)