Erdős Problem a Daythe open tracker
The board / number theory / #431

Erdős Problem #431
inverse Goldbach problem

OPENdatabase updated 2025-08-31

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).

Are there two infinite sets \(A\) and \(B\) such that \(A+B\) agrees with the primes up to finitely many exceptions? This was disproved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/431.
Newer public claim (6 Oct 2026): OpenAI's internal-model release claims, for this problem, Ostmann: no finite modification of the primes is a sumset A+B — read by four AI referee seats here 23 Oct, see /day/431-openai-ostmann-inverse-goldbach-refereed — family 13 at github.com/openai/math, OpenAI's own Lean proves Theorem 1.1 — (A+B) △ primes is infinite whenever |A|, |B| ≥ 2 — twice, by two developments that share 47 of about 7,500 modules: route C (Complete.lean, comparator OstmannComplete) formalizes the paper's analytic inputs and discharges each by a proof; route M (Main.lean, comparator OstmannPrimes) uses instead a Lean proof that Landau–Siegel zeros do not exist, a claim from the release's family 003 that the paper does not use. Kernel-replayed on our machine on 23 Oct 2026 — 7,582 modules, 0 errors, standard axioms, both comparator statements matched under pp.all; the no-Siegel-zero theorem's statement checked against our own root-namespace copy in Mathlib's definitions. leanchecker --fresh over Mathlib and both routes exited 0. Kernel-checked bridges of ours prove Formal Conjectures' erdos_431 and erdos_431.variants.ostmann from each route — see our /day entry. Bloom calls these claims, not endorsements.
Prizenone
Topicsnumber theory, primes
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/431

Attempts

submit one →
FULL WRITE-UP BY THIS SITE · OCT 23, 2026

Read our full write-up →

Are there infinite sets A and B whose sumset A + B equals the primes up to finitely many exceptions? Ostmann asked it in 1956 and Erdős recorded it; the best results were square-root bounds on how thin A and B would have to be. OpenAI's preprint of 24 September (80 pages, family 013) proves the answer is no, and more: for any A, B with at least two elements each, A + B differs from the primes in infinitely many places. Four AI referee seats read §§1–9 and found no gap, only exposition notes. Its Lean has two comparator challenges proved by two almost disjoint developments (47 shared modules of about 7,500). Route C formalizes the paper's own analytic inputs; route M instead goes through a Lean theorem that Landau–Siegel zeros do not exist, a claim from the release's family 003 (uniform exclusion of Landau–Siegel zeros) that the paper does not use. We replayed all 7,582 modules (0 errors, standard axioms, statements matched) and wrote that theorem's statement ourselves in Mathlib's own L-functions: the kernel accepts OpenAI's proof of our copy. Nobody here has refereed that proof. Ours: Formal Conjectures' two #431 statements, proved in Lean from each route. The theorem is OpenAI's.

CLOSED
← #430the board#432 →