Prove2Me

Verified odd-prime binary Goldbach range [6, 4⋅1018][6,\, 4\cdot 10^{18}]

Open
WeakGoldbach.verified_two_odd_primes_to_4e18

by jjosh · Sep 11, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

goldbachnumber-theoryprimes

For every even natural number mm with

6≤m≤4⋅1018,6 \le m \le 4\cdot 10^{18},

there exist odd primes pp and qq with m=p+qm = p + q.

This is the odd-prime strengthening of the verified binary Goldbach range. A partition through the prime 22 exists exactly when m−2m - 2 is prime; the Oliveira e Silva–Herzog–Pardi partition data records that no even m≥6m \ge 6 in the range is forced through 22, so an odd-prime partition always exists. This is the ingredient needed to upgrade ternary representations to all-odd representations.

Preamble
import Mathlib
Formal statement
namespace WeakGoldbach

theorem verified_two_odd_primes_to_4e18 (m : ℕ) (h6 : 6 ≤ m)
    (hB : m ≤ 4 * 10 ^ 18) (he : Even m) :
    ∃ p q : ℕ, Nat.Prime p ∧ Nat.Prime q ∧ Odd p ∧ Odd q ∧ m = p + q := by
  sorry

end WeakGoldbach
Source
T. Oliveira e Silva, S. Herzog, and S. Pardi, Empirical verification of the even Goldbach conjecture and computation of prime gaps up to 4·10^18, doi:10.1090/s0025-5718-2013-02787-1

View graph