Goldbach's Conjecture

import Mathlib

-- Every even integer greater than 2 is the sum of two primes.
theorem goldbach (n : ℕ) (hn : 2 < n) (heven : Even n) :
    ∃ p q : ℕ, Nat.Prime p ∧ Nat.Prime q ∧ p + q = n :=