Verified binary Goldbach range through $4\times 10^{18}$

Open

WeakGoldbach.verified_two_primes_to_4e18

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

goldbachnumber-theoryprimes

This is the Oliveira e Silva–Herzog–Pardi distributed verification of the even (binary) Goldbach conjecture.

For every even natural number $m$ with

4 \le m \le 4\cdot 10^{18},

there exist primes $p$ and $q$ with

m = p + q.

In the proof of the ternary Goldbach conjecture, this computation is the base on which the Helfgott–Platt prime ladder rests: for an odd $n$ , one chooses a ladder rung $p$ below $n$ so that $n - p$ is a positive even number inside this verified range, and concludes $n = p + q + r$ .

Formalization Note The statement is over Nat with the bound $m \le 4\cdot 10^{18}$ ; the summand order is $m = p + q$ .

Preamble

import Mathlib

Formal statement

namespace WeakGoldbach

theorem verified_two_primes_to_4e18 (m : ℕ) (h4 : 4 ≤ m)
    (hB : m ≤ 4 * 10 ^ 18) (he : Even m) :
    ∃ p q : ℕ, Nat.Prime p ∧ Nat.Prime 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, Math. Comp. 83 (2014), no. 288, 2033–2060, DOI 10.1090/S0025-5718-2013-02787-1; used as the binary base in Helfgott–Platt, arXiv:1305.3062v2, §1 and §4

View graph

Verified binary Goldbach range through 4×10184\times 10^{18}4×1018

Verified binary Goldbach range through $4\times 10^{18}$