∑math20

Number theory · Result 013

Ostmann’s inverse Goldbach conjecture

1 paperLean

Proves that no finite modification of the primes can be written as \(A+B\) with \(A,B\subseteq\mathbb Z_{\ge0}\) each containing at least two elements. This resolves Ostmann's inverse Goldbach conjecture on additive indecomposability.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of The additive indecomposability of the primes

The additive indecomposability of the primes

OpenAI · September 24, 2026

We prove Ostmann's inverse Goldbach conjecture: no set differing from the primes by finitely many elements can be written as \(A+B\), where A and B are sets of nonnegative integers with at least two elements each.

Read PDF Download Source

Cite
@misc{OAI:the-additive-indecomposability-of-the-primes-September-24-2026,
  author = {{OpenAI}},
  title = {{The additive indecomposability of the primes}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/the-additive-indecomposability-of-the-primes-September-24-2026/paper.pdf}{OAI:the-additive-indecomposability-of-the-primes-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalization proves Ostmann's inverse Goldbach conjecture. For any two sets \(A,B\) of nonnegative integers, each containing at least two elements, the symmetric difference between their sumset \(A+B\) and the set of primes is infinite. Thus no set differing from the primes by only finitely many elements can be decomposed as such a sumset. The linked statements include the full result and its two-infinite-summands case.

Comparator links

ResultComparator statement
Ostmann's inverse Goldbach theorem and the infinite-summands caseOstmannComplete.lean
Additive indecomposability of the primes up to finite changesOstmannPrimes.lean

Scope note on GitHub →