Proves Erdős’s conjecture that every set of positive integers with divergent reciprocal sum contains arithmetic progressions of every finite length. Quantitatively, for each fixed k ≥ 3, every subset of \(\{1,\ldots,N\}\) with no nonconstant k-term progression has size at most \(C_kN\exp[-c_k(\log N)^{\varepsilon_k}]\), with positive constants depending only on k. (OpenAI’s Lean note)
Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.
The independent assessments find that the Lean statements express only part of the result described above, or a narrower statement. Read the assessments
It bears on Erdős problem #3, as listed by Thomas Bloom, erdosproblems.com.
In Quasipolynomial Bounds for Arithmetic Progressions, 23 September 2026
Possible match to OpenAI’s description, selected from shared wording. No review confirming the selection is recorded.
Every set A\subseteq\mathbb N with \sum_{a\in A}a^{-1}=\infty contains nonconstant arithmetic progressions of every finite length.
In Quasipolynomial Bounds for Arithmetic Progressions, 23 September 2026
Possible match to OpenAI’s description, selected from shared wording. No review confirming the selection is recorded.
For each fixed integer k\ge3 there are constants C_k,c_k,\varepsilon_k>0 such that, for every N\ge2,
Equivalently, there is A_k\ge1 such that an \alpha-dense subset of [N] contains a nonconstant k-term progression whenever
No Lean statement in the release is paired with this theorem.
The release does not say which paper theorem its catalogue describes. The statements above share the most wording with the description; the atlas has not reviewed that choice. Identifying it is listed under Questions awaiting review.
Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.
OpenAI released an abridged summary of the model’s reasoning for this family: Quasipolynomial bounds for arithmetic progressions
Lean is a language for mathematical statements and proofs that a computer can verify. The Lean statement below is shown beside its possible paper counterpart, with the reason they were linked.
For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.
ErdosReciprocalThe paper states
In Quasipolynomial Bounds for Arithmetic Progressions, 23 September 2026
Every set A\subseteq\mathbb N with \sum_{a\in A}a^{-1}=\infty contains nonconstant arithmetic progressions of every finite length.
The words they share: arithmetic, contains, divergent, finite, length, progressions, reciprocal.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
ErdosReciprocal.lean, the release lists it as a supporting statement.
def ReciprocalProgressionTheorem : Prop := ∀ A : Set ℕ, ¬ Summable (reciprocalTerm A) → ∀ k : ℕ, HasAP A ktheorem manuscriptReciprocalProgressionTheorem : ReciprocalProgressionTheorem := by sorryThis file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
two independent groups report that Comparator accepted runs for this Lean statement file: MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program
Atlas found these propositions by scanning the text of the project’s Model.lean file. Each name links to its definition, with any associated statement file beside it. This list does not record running Lean to interpret or verify those definitions.
HasAP Model.lean, line 7APFree Model.lean, line 10QuantitativeDensityBound Model.lean, line 31QuantitativeDensityTheorem Model.lean, line 37ReciprocalProgressionTheorem Model.lean, line 40The source scan also found 5 theorem or lemma declarations whose names contain ‘manuscript’.
Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.
MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.
MathVet finds that the Lean statements express part of the advertised result (their term: “partial”).
Their note: ReciprocalProgressionTheorem : ∀ A : Set ℕ, ¬ Summable (reciprocalTerm A) → ∀ k, HasAP A k (HasAP: a k-term progression a + i·d, d > 0, inside A) is exactly the first claim, stated for all A ⊆ ℕ (0 ∈ A is harmless: it contributes 0 to the sum and the positive-integer case is covered). The paper’s quantitative bound |A| ≤ C_k N exp(-c_k (log N)^ε_k) for k-AP-free subsets of {1..N} has no statement (docs: ‘outside this statement’); the solution cone is by far the largest in this set (4,774 files, 1,122,983 OAI lines).
“partial”, in their words: Only a special case is stated, or a co-equal headline claim has no challenge statement.
Their method: An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
cert-machine finds that the Lean statements express a narrower statement than the advertised result (their term: “NARROWER — DECLARED”).
The gap they name: The quantitative Szemerédi bound for k-AP-free subsets of {1,…,N} is not stated.
“NARROWER — DECLARED”, in their words: The challenge statements state less than the headline, and OpenAI’s Lean note says so.
Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.
OpenAI’s own note on what its Lean covers
Erdős’s reciprocal-sum conjecture asks whether every set of positive integers with divergent reciprocal sum contains arithmetic progressions of every finite length. The formalization proves this statement: for every requested length, such a set contains a progression with positive common difference.
The selected theorem is the reciprocal-sum consequence. The paper’s quantitative upper bound for the largest progression-free subset of $\{1,\ldots,N\}$ is outside this statement.
Erdős’s reciprocal-sum arithmetic-progression conjecture ErdosReciprocal
Unreviewed AI draft: states a consequence of a paper’s theorem. States the reciprocal-sum corollary (Erdős’s conjecture), which the paper derives from its quasipolynomial bound for sets without k-term progressions. The bound itself is outside the statement.
These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.
These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.
ErdosReciprocalThree reports, all at the release’s recorded version.
| Reported by | Their word | Their account | Date | Original report |
|---|---|---|---|---|
| cert-machine | “REFUSED” | Re-run through Comparator did not reach a verdict (the job stopped before Comparator ran (see the run log)). | 10 October 2026 | Original report |
| MathVet | “comparator-pass” | Re-run through Comparator: accepted. | 8 October 2026 | Original report |
| Neal McBurnett, openai-math-lean-tooling | “accepted” | Re-run through Comparator with Lean’s kernel: accepted (the check took 2472 s; peak memory 14.3 GiB). | 10 October 2026 | Original report |
Other people’s accounts of running proof-verification software, with links to their reports.
plasma-ai, site erdosproblems.ai, plasma-ai/erdos: an open record of the Erdős problems with claim pages for the OpenAI release, 8 October 2026. Source
Problem 3 claim page records OpenAI’s reciprocal-sum corollary as accepted after the corpus built and audited the Lean declaration.
Explanations of this family written elsewhere, by the people named. Each is their own reading of the mathematics.
seaworld008, seaworld008/openai-math-top30: thirty selected families explained in Chinese, 7 October 2026. Source
Chinese-language explainer for general readers, with a beginner’s section, a specialist section, background on why the problem was hard and a diagram; it ends by saying it paraphrases OpenAI’s summary and does not represent consensus.
The program that collects Atlas’s source records, Statement Map, could not obtain or interpret some source material. These notes describe those limits; they do not identify mathematical errors.
ErdosReciprocal: Tracked source lean/OAI/Combinatorics/Progressions/Main.lean unavailable: bytes were not captured at fd4aeeb2ee4fc729c18d98444fed42fd0529eeebThese links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.
The Justin Sun Prize, The Justin Sun Prize: problem bank and award records, 11 October 2026. Source
JSP-000044 lists the release’s claim as Solved with independent mathematical review pending; Lean proof column: reported complete, independent verification pending.
Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release
Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.
Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.
Offer to write an explanationCompare the Lean statement with the paperSuggest a source attributionSuggest a change
Commentary on this family by others, dated and credited. It is commentary, not a finding.
An unsigned public tier list, the OpenAI Math Tier List, classes it as a proof and rates its significance, if it holds up, as “Would win a Fields Medal”. The page says that nothing on it is verified.
Author not stated. Source
Moritz Firsching, anxkhn, Paul Lezeau, Formal Conjectures: mark problems solved in the OpenAI math release and link formal proofs, 11 October 2026. Source
A Formal Conjectures maintainer, after source inspection, links the quasipolynomial Szemeredi bound to Erdos problem 3.
OfficeChai (byline not recorded), OpenAI Has Also Included Proofs For 23 Erdos Problems In Its Latest Math Proof Drop, 9 October 2026. Source
Erdos #3: a quasipolynomial-type Szemeredi bound for all progression lengths would imply the reciprocal-sum conjecture; Lean file currently proves only a weaker bound.
MalekZ, jleng01, NicoV, efiebig, Thomas Bloom, Comments on ‘Erdős problems in the OpenAI proofs’, 9 October 2026. Source
One commenter who spent an hour on this manuscript found notation with several meanings that needed back-tracking, and another who has worked on the problem says the 200 pages are mainly useful for another AI to explain to a human.
Thomas Bloom, Erdős problems in the OpenAI proofs, 8 October 2026. Source
Bloom lists Erdős 3 as a claimed proof in a 198-page PDF, names Kelley and Meka (three-term case) and Leng, Sah and Sawhney as earlier work, and notes that the challenge file states only the reciprocal-sum consequence while the Lean code appears to prove a weaker quantitative bound than the PDF.
Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.
Why this passage is shown
Corollary 1.2 (Divergent reciprocal sums)
In Quasipolynomial Bounds for Arithmetic Progressions, 23 September 2026
Why this passage is shown
Theorem 1.1
In Quasipolynomial Bounds for Arithmetic Progressions, 23 September 2026
Independent assessment
MathVet
14c7f91Independent assessment
Carlos Toledo’s cert-machine
9814e4cProof-verification report
cert-machine, ErdosReciprocal
Proof-verification report
MathVet, ErdosReciprocal
Proof-verification report
Neal McBurnett, openai-math-lean-tooling, ErdosReciprocal
Lean statement
ErdosReciprocal