Weak Goldbach for $n = 5$ : singleton prime multiset

Open

WeakGoldbach.three_primes_five

by junyihjy · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

goldbachnumber-theoryweak-goldbach

The number $5$ is the sum of at most three primes: the singleton multiset $\{5\}$ has cardinality $1 \le 3$ , its only member $5$ is prime, and its sum is $5$ . This is one of the two small cases ( $n = 3$ and $n = 5$ ) in the mission's proof approach, complementing Helfgott's theorem which supplies three odd primes for odd $n > 5$ .

Preamble

import Mathlib

set_option autoImplicit false

Formal statement

theorem WeakGoldbach.three_primes_five :
    ∃ s : Multiset ℕ, s.card ≤ 3 ∧ (∀ p ∈ s, Nat.Prime p) ∧ s.sum = 5 := by sorry

View graph

Weak Goldbach for n=5n = 5n=5: singleton prime multiset

Weak Goldbach for $n = 5$ : singleton prime multiset