Dubner's conjecture

Reference: Every even number greater than 4208 is the sum of two t-primes by Harvey Dubner.

def DubnerConjecture.IsTwinPrime (p : ℕ) : Prop

A twin prime is a prime number that has a prime gap of 2, meaning either p - 2 or p + 2 is also prime.

Equations

• DubnerConjecture.IsTwinPrime p = (Nat.Prime p ∧ (Nat.Prime (p - 2) ∨ Nat.Prime (p + 2)))

theorem DubnerConjecture.t1 : ¬IsTwinPrime 2

theorem DubnerConjecture.t2 : IsTwinPrime 3

theorem DubnerConjecture.t3 : IsTwinPrime 5

theorem DubnerConjecture.t4 : IsTwinPrime 101

theorem DubnerConjecture.t5 : ¬IsTwinPrime 100

theorem DubnerConjecture.dubner_conjecture (n : ℕ) (hn : 4208 < n) (h : Even n) : ∃ (p : ℕ) (q : ℕ), IsTwinPrime p ∧ IsTwinPrime q ∧ p + q = n

Every even number greater than 4208 is the sum of two twin primes.