Erdős Problem #3
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
Attempts
submit one →Read our full write-up →
Erdős's $5000 question — does a divergent reciprocal sum force arithmetic progressions of every length? — was open for every k ≥ 4; the best bound (Leng–Sah–Sawhney 2024) fell short of the dyadic-summability threshold. OpenAI's 23 September 2026 paper claims r_k(N) ≤ C_k·N·exp(−c_k(log N)^ε_k) for every k in 198 machine-written pages; the Lean it ships proves a different, weaker bound, exp(−c(log log N)^(1+η)), that is nonetheless past the threshold and so proves the reciprocal-sum statement itself — exactly the question on the problem page — in a 4,774-file, 1.1-million-line proof we audited at source (no sorry, no axioms, no escape hatches; statement identical to the challenge) and replayed on our own machine — 13,697 jobs built from the pinned sources in 14.3 hours, and under --trust=0 the kernel printed exactly propext, Classical.choice and Quot.sound for the reciprocal-sum theorem, the quantitative bound and their conjunction, with the challenge statement identical to the solution's under pp.all; nobody else had reported building it with a log (Formal Conjectures marked the problem solved on source inspection). Seven hostile seats read the paper in disjoint scopes against the sources of its two external inputs: holds as read, seven of seven — no mathematical gap, no constant cycle, the exponent iteration-independent by the paper's own argument, about forty exposition notes. Not ours — but our kernel has now said so, and #3 joins the problems closed in the literature.
CLOSED