Goldbach's conjecture

The arithmetic proposition used by the Goldbach machine semantics.

def ConjectureMachines.GoldbachConjecture : Prop

Every even natural number greater than two is the sum of two primes.

Equations

• ConjectureMachines.GoldbachConjecture = ∀ (n : ℕ), 2 < n → Even n → ∃ (p : ℕ), ∃ (q : ℕ), Nat.Prime p ∧ Nat.Prime q ∧ n = p + q