Goldbach's conjecture

References:

• Landau Problems Wikipedia Page
• Goldbach's Conjecture Wikipedia Page

theorem GoldbachConjecture.goldbach (n : ℕ) (hn : 2 < n) (hn_even : Even n) : ∃ (p : ℕ) (q : ℕ), Prime p ∧ Prime q ∧ n = p + q

Can every even integer greater than 2 be written as the sum of two primes?

theorem TernaryGoldbachConjecture.ternaryGoldbach (n : ℕ) (hn : 5 < n) (hn_odd : Odd n) : ∃ (p : ℕ) (q : ℕ) (r : ℕ), Nat.Prime p ∧ Nat.Prime q ∧ Nat.Prime r ∧ n = p + q + r

Can every odd integer greater than 5 be written as the sum of three primes? (A prime may be used more than once.)

NB. While Harald Helfgott's solution is not published in a peer-reviewed journal yet, his results seem generally accepted.