Prove2Me

Finite binary Goldbach verification through 4⋅10184\cdot10^{18}

Open
WeakGoldbach.even_goldbach_to_4e18

by con · Sep 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

computational-number-theorygoldbachnumber-theory

Every even natural number in the verified range

4≤n≤4⋅10184\le n\le 4\cdot10^{18}

is the sum of two primes:

n=q+r.n=q+r.

Repetition of the primes is permitted. This is the finite binary Goldbach input used by Helfgott and Platt to lift a prime ladder to their ternary verification range. It asserts no case above the stated bound. The computational verification remains an open formal proof obligation.

Preamble
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Algebra.Ring.Parity
Formal statement
theorem WeakGoldbach.even_goldbach_to_4e18
    (n : ℕ) (hlo : 4 ≤ n) (hhi : n ≤ 4 * 10 ^ 18) (heven : Even n) :
    ∃ p q : ℕ, Nat.Prime p ∧ Nat.Prime q ∧ n = p + q := by sorry
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, Math. Comp. 83 (2014), 2033-2060, abstract (p. 2033), DOI 10.1090/S0025-5718-2013-02787-1; author abstract: https://sweet.ua.pt/tos/bib/4.12.html . Also H. A. Helfgott and D. J. Platt, arXiv:1305.3062v2, Section 1, p. 1, final paragraph: https://arxiv.org/abs/1305.3062

View graph