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

Your AI and this story

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