Goldbach's Conjecture
Open
Theorem
1
2
3
-- 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 :=
-- 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 :=