Goldbach_Conjecture_implies_Weak_Goldbach_Conjecture
Provedgoldbachnumber-theoryproofwiki
The Goldbach Conjecture implies Goldbach's Weak Conjecture.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Data.Nat.Prime.Basic
Formal statement
theorem Goldbach_Conjecture_implies_Weak_Goldbach_Conjecture (goldbach : ∀ n : ℕ, n > 2 → n % 2 = 0 → ∃ p q : ℕ, Nat.Prime p ∧ Nat.Prime q ∧ n = p + q) : ∀ n : ℕ, n > 7 → n % 2 = 1 → ∃ p q r : ℕ, Nat.Prime p ∧ Nat.Prime q ∧ Nat.Prime r ∧ n = p + q + r := by sorry
Source