Lemoine's conjectures

References:

• Wikipedia
• [Ki85] Kiltinen, J. and Young P. (1985). Goldbach, Lemoine, and a Know/Don't Know Problem.

def Lemoine.OddPrime (n : ℕ) : Prop

Equations

• Lemoine.OddPrime n = (n ≠ 2 ∧ Nat.Prime n)

theorem Lemoine.lemoine_conjecture (n : ℕ) (hn : 6 < n) (odd : Odd n) : ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ Nat.Prime q ∧ p + 2 * q = n

For all odd integers $n ≥ 7$ there are prime numbers $p,q$ such that $n = p+2q$.

theorem Lemoine.lemoine_conjecture_extension (n : ℕ) (hn : 8 < n) (odd : Odd n) : ∃ (p : ℕ) (q : ℕ) (r : ℕ) (s : ℕ) (a : ℕ) (b : ℕ), OddPrime p ∧ OddPrime q ∧ OddPrime r ∧ OddPrime s ∧ p + 2 * q = n ∧ 2 + p * q = 2 ^ a + r ∧ 2 * p + q = 2 ^ b + s

For all odd integers $n ≥ 9$ there are odd prime numbers $p,q,r,s$ and natural numbers $a,b$ such that $p+2q = n$, $2+pq = 2^a+r$, $2p+q = 2^b+s$