Ostmann's inverse Goldbach conjecture

Ostmann's inverse Goldbach conjecture asserts that the primes are additively indecomposable up to finite changes: no set that differs from the primes in only finitely many elements is a sumset A + B of two sets of nonnegative integers with at least two elements each. Erdős recorded the two-infinite-sets form as Problem 431 on the Erdős problems site. A manuscript dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims the conjecture, with a Lean formalization. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

Background

• As recounted in the introduction of the manuscript:
  • Ostmann stated the conjecture in his 1956 treatise; the eventual-equality formulation is recorded by Elsholtz and Harper. Laffer and Mann showed that a decomposition would need two infinite summands.
  • Sieve arguments of Hornfeck, Pomerance–Sárközy–Stewart, Hofmann–Wolke and Elsholtz restricted a hypothetical decomposition. Elsholtz ruled out three nontrivial summands, and Elsholtz and Harper showed that each summand of a binary decomposition has between about the square root of x divided by log x log log x and about the square root of x times log log x elements up to x.
  • Green and Harper showed that an inverse large sieve conjecture would imply Ostmann's conjecture; Hanson, Croot–Mao–Yip and Croot–Mao–Pohoata–Yip proved partial inverse results and further necessary conditions.
• The Erdős problems page for Problem 431 (accessed 17 October 2026; last edited 8 April 2026) records these and related results and lists no proof claims.

The original result

• Additive indecomposability of the primes (24 September 2026). The manuscript's main statement is that if A and B are sets of nonnegative integers with at least two elements each, then the symmetric difference of A + B and the primes is infinite. It first reduces to two infinite summands by a short sieve argument and then proves a contradiction for that case.
  • Method, as described: residue images of the summands modulo each prime are completed to a partition and shown to be approximately balanced. Persistent correlations with translated multiplicative characters are excluded, first for quadratic characters by a moment argument, Poisson summation and the quadratic large sieve, and then for higher orders by repeated Cauchy–Schwarz transfers. A tensor estimate uses coverage of the primes, and a finite-field comparison for the resulting binary trees and a positive statistic lead to the final contradiction. The manuscript states that it does not need Green and Harper's inverse sieve conjecture.
• Sources. Commit 1581d4c of the openai/math repository, folder The additive indecomposability of the primes.
• Formalization, as described by the repository. The scope note lean/docs/013.md states that the formalization proves the conjecture: for any two sets of nonnegative integers with at least two elements each, the symmetric difference of their sumset and the primes is infinite. The Comparator statements are OstmannComplete (the full result and the two-infinite-summands case) and OstmannPrimes.
• Kernel records. In the con-leche development journal's run over all 416 Comparator challenges of the collection (repository commit fd4aeeb, run of 10 October 2026; DESIGN.md, task #348), con-leche and Lean's official kernel both accepted 401 challenges; neither Ostmann statement is among the 15 named exceptions.
• Catalogue status. In Formal Conjectures, the statement of Erdős Problem 431 and its Ostmann variant are marked solved on the main branch, with formal proof links to the openai/math Lean files at commit adc7f12 (ErdosProblems/431.lean).

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 17 October 2026)
2026-10-11	P. Leonetti, arXiv:2610.15758 (v1), titled On the inverse Goldbach problem	Remark (related work)	If A + B differs from the primes in only finitely many elements, with both sets of at least two elements, then the counting functions of A and B lie between constant multiples of the square root of x divided by log x and of the square root of x. A second result bounds below the symmetric difference of a three-term sumset and the primes. The introduction states that OpenAI announced a proof of Ostmann's conjecture and that at the time of writing this claim had not yet been verified by the math community.	arXiv v1.

Notes

• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.