Goldbach's conjecture

Reference: Wikipedia

theorem 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?