Goldbach conjecture

Conjectura.Statements.Mathematics.NumberTheory.GoldbachConjecture

/-
Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors
-/
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Algebra.Group.Even

/-! # Goldbach conjecture -/

namespace Conjectura.NumberTheory

/-- The **Goldbach conjecture**: every even number greater than two is a sum of two primes. -/
def GoldbachConjectureProp : Prop :=
  ∀ n : ℕ, 2 < n → Even n → ∃ p q : ℕ, p.Prime ∧ q.Prime ∧ n = p + q

end Conjectura.NumberTheory