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?