AI Proved What?

Episode 013, October 2026

Split the primes?

Ostmann’s inverse Goldbach conjecture: the primes are additively indecomposable

Covers result 013 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.

Play Episode 013: Split the primes? Ostmann’s inverse Goldbach conjecture, Erdős problem 431. A clock of residues mod 7, with the residues of A in blue and those of minus B in orange, never meeting.

4:23. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00Splitting a set
  2. 0:44A near miss
  3. 1:36The residue clock
  4. 2:17The claim
  5. 2:34How the proof goes
  6. 3:27Lean, and the caveats

The claim, in plain words

For sets A and B of nonnegative integers, A + B is the set of all sums a + b. Many sets split this way: every number from 10 on is {0, 1} plus the even numbers from 10 on. In his 1956 book Additive Zahlentheorie, Hans-Heinrich Ostmann conjectured that the primes do not: no two sets, each with at least two elements, have exactly the primes as their sums, even after adding or removing finitely many numbers. This is the inverse Goldbach problem, and Erdős problem #431.

Result 013 claims to prove it: if |A|, |B| ≥ 2, then A + B and the primes differ in infinitely many numbers. Either infinitely many primes are not sums, or infinitely many composite numbers are.

What it doesn’t claim

The condition that both sets have at least two elements matters: {0} plus the primes is the primes. The result is qualitative; it gives no bound on how many exceptions there must be up to x.

Where it stands

Posted as a preprint
OpenAI, dated September 24, 2026; released October 6, 2026
Peer reviewed
Not yet
Checked in Lean
OpenAI published two separate Lean proofs of the main theorem (scope note); we have not run the check

Last checked October 19, 2026. The claim has not been withdrawn, and we found no public critique. Erdős problem #431 is still listed as open on erdosproblems.com.

What was known

  • Hornfeck (1954) began the restrictions on a hypothetical decomposition, and Laffer and Mann (1964) showed that both summands would have to be infinite.
  • Elsholtz (2001) showed that each summand would have about √x elements up to x, up to powers of log x, and ruled out writing the primes as a sum of three such sets; Elsholtz and Harper (2015) sharpened the bounds to √x/(log x log log x) ≪ A(x), B(x) ≪ √x log log x.
  • Green and Harper (2014) showed that an inverse large sieve conjecture, classifying sets that occupy about half the residues mod many primes, would imply Ostmann’s conjecture. Hanson, Croot, Mao, Pohoata and Yip proved partial results in that direction.

How the proof goes

  1. Two infinite sets. A short sieve argument reduces to the case where both summands are infinite.
  2. Residue clocks. Put D = −B. Every large sum is a prime larger than any fixed prime p, so, after setting aside small elements, A and D occupy disjoint residues mod p. A collision estimate shows that, on average over primes, the two parts are about equal in size.
  3. No structure. The summands cannot correlate with quadratic characters, even with centres that move from prime to prime; higher-order characters follow by repeated Cauchy–Schwarz transfers.
  4. Coverage. Every large prime must be a sum. A positive statistic built from this coverage is compared, through a finite-field comparison of binary trees, with what the decorrelation allows; the two cannot both hold. The proof does not use the Green–Harper conjecture.

The Lean statement

theorem main : ∀ A B : Set ℕ, A.Nontrivial → B.Nontrivial →
    Set.Infinite ((A + B) ∆ {n : ℕ | Nat.Prime n})

This is the statement in the challenge file: Nontrivial means at least two elements, and ∆ is the symmetric difference. The proof behind it is about 4,400 files of OpenAI’s code, about 365,000 lines; a second, separate Lean proof of the same theorem by a different route adds about 3,200 files. A passing Comparator check would guarantee the statement from Lean’s standard axioms. Neither proof is in OpenAI’s formalization catalog yet, and we have not run the check.

The near miss in the video

  • A = {0, 6} and B = the primes p with p + 6 also prime (5, 7, 11, 13, 17, 23, 31, …). Every sum is prime.
  • Below 200 it misses exactly the primes 2, 3, 71, 127, 139, 149 and 181. Up to 106 it misses 62% of the primes (29,872 of 78,498 are covered). Here |A| = 2 while B has 16,386 elements below 106: far from the balanced √x sizes a real decomposition would need.
  • Mod 7, A gives the residues {0, 6} and −B (for b > 7) gives {1, …, 5}: they never meet.
  • Checked with a short Python script.

Read the source

The paper

OpenAI groups related papers into one result; this one has a single paper.

Transcript

Read the full script

0:00Splitting a set

Take two sets of numbers, A and B, and form every sum: one element of A plus one element of B. Lots of sets arise this way. Every number from 10 on is 0 or 1, plus an even number from 10 on. Can the primes be built like this? In his 1956 book, Hans-Heinrich Ostmann conjectured that they can’t: no two sets with at least two elements each have exactly the primes as their sums, even if you may add or remove finitely many numbers. It is called the inverse Goldbach problem, and it is Erdős problem #431. Result 013 in OpenAI’s math repository claims to prove Ostmann’s conjecture, and a Lean proof comes with it.

0:44A near miss

Here’s a try. Let A be {0, 6}, and let B be the primes p for which p + 6 is also prime: 5, 7, 11, 13, 17, and so on. Then every sum is prime, by design. But does it hit every prime? Below 200, it misses only seven: 2, 3, 71, 127, 139, 149, and 181. Up to a million, it misses 62%. Pairs of primes 6 apart thin out, and the misses take over. So a decomposition would have to be balanced. In 1964, Laffer and Mann showed that both sets would have to be infinite. Christian Elsholtz later showed that each would have roughly the square root of x elements up to x, give or take logarithms, and ruled out writing the primes as a sum of three such sets.

1:36The residue clock

Here is the constraint that drives the proof. Pick a prime q. Every large sum, a + b, is a prime bigger than q, so q doesn’t divide it. So, setting aside small elements, a is never congruent to −b, modulo q. On the clock of residues mod q, A and −B live in separate hours. In a real decomposition, this would happen for every prime q at once, and on average the two sets would split each clock roughly in half. Sets like that look structured, like the perfect squares. Ben Green and Adam Harper showed that a conjecture classifying such sets would imply Ostmann’s conjecture. That classification is still unproven.

2:17The claim

Result 013 claims Ostmann’s conjecture outright. If A and B each have at least two elements, then the sums and the primes differ in infinitely many numbers. Either infinitely many primes are missed, or infinitely many composite numbers sneak in.

2:34How the proof goes

First, a short sieve argument reduces to two infinite sets. Then the clocks: with D = −B, and small elements set aside, A and D occupy disjoint residues mod every prime, and a counting estimate shows that, on average, they split each clock almost evenly. Next, the paper rules out structure. It shows that the two sets can’t correlate with quadratic patterns, like the squares, at shifting centers, and then with higher-order multiplicative patterns, through repeated Cauchy–Schwarz transfers. Finally, it uses the fact that every large prime must be covered. A positive statistic built from that coverage is compared with what the decorrelation allows, through a finite-field comparison of binary trees. The two can’t both hold. Notably, it never needs Green and Harper’s conjecture.

3:27Lean, and the caveats

The Lean statement takes two lines: for any sets A and B of natural numbers, each with at least two elements, the symmetric difference between A + B and the primes is infinite. The proof behind it is huge: about 4,400 files of OpenAI’s code, more than 360,000 lines. A second, separate Lean proof adds about 3,200 more files. A passing Comparator check would guarantee the statement from Lean’s usual axioms. OpenAI’s catalog of formal proofs doesn’t list it yet, and we haven’t run the check ourselves. The caveats. This is a preprint, 80 pages, not peer reviewed. And Erdős problem #431 is still listed as open. The primes aren’t a sum of two sets with two or more elements each, not even up to finitely many changes. If the proof holds. And a computer can check it.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.