Dubner's conjecture: Twin prime sums

[franzhusch]

What is the conjecture

A twin prime is a prime number $p$ such that either $p + 2$ or $p - 2$ is also prime. Dubner's conjecture asserts that every even number greater than $4208$ can be expressed as the sum of two primes which both have twins. In other words, for all $n > 4208$ with $n$ even, there exist twin primes $p$ and $q$ such that $p + q = n$.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

Sources:

• https://en.wikipedia.org/wiki/Twin_prime#Dubner's_conjecture, https://oeis.org/A081947, https://www.primepuzzles.net/conjectures/conj_032.htm

Prerequisites needed

Formalizability Rating: 1/5 (0 is best) (as of 2026-03-24)

Building blocks (1-3; from search results):

• Prime (from Mathlib.Algebra.Prime.Defs): definition of prime elements in commutative monoids with zero
• Natural number arithmetic and ordering (available in Mathlib)
• Even number predicate (available in Mathlib.Data.Nat.Parity)

Missing pieces (exactly 2; unclear/absent from search results):

• IsTwinPrime helper definition: a simple predicate asserting that a prime $p$ has a twin (either $Prime(p+2)$ or $Prime(p-2)$)
• Formalization of the upper bound verification (checking all even numbers $\leq 4208$, though this may be computational)

Rating justification (1-2 sentences): The core concepts (primes, sums, even numbers) all exist in Mathlib. Only a simple one-line helper predicate for twin primes is needed to state the conjecture, making formalization straightforward.

AMS categories

• ams-11

Choose either option

• I plan on adding this conjecture to the repository
• This issue is up for grabs: I would like to see this conjecture added by somebody else

---

This issue was generated by an AI agent and reviewed by me.

If you have feedback on mistakes / hallucinations, feel free to just write it in the issue. See more information here: link

[ellow0rld]

There is already a file for the Twin Prime Conjecture (TwinPrimes.lean). We could add Dubner’s Conjecture as a variant there; however, it doesn't appear to have a dedicated Wikipedia entry. Since it is primarily documented in academic papers. it technically belongs under FormalConjecture/Paper per the repo's structure.