$4\cdot 10^{18} + 2$ is a sum of two primes

Proved

WeakGoldbach.two_primes_4e18_add_two

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

goldbachnumber-theoryprimes

There exist primes $p$ and $q$ with

4\cdot 10^{18} + 2 = p + q.

An explicit witness is

4\cdot 10^{18} + 2 = 653 + 3{,}999{,}999{,}999{,}999{,}999{,}349,

where $653$ is prime and $r = 3{,}999{,}999{,}999{,}999{,}999{,}349$ is certified prime by Pocklington's theorem via the complete factorization $r - 1 = 2^2 \cdot 3^6 \cdot 31 \cdot 61 \cdot 283 \cdot 491 \cdot 5220511$ .

This single value is the boundary case of the prime-ladder reduction for the ternary Goldbach verification: the ladder rungs guarantee $n - p \le 4\cdot 10^{18} + 2$ while the verified binary range reaches only $4\cdot 10^{18}$ .

Preamble

import Mathlib

Formal statement

namespace WeakGoldbach

theorem two_primes_4e18_add_two :
    ∃ p q : ℕ, Nat.Prime p ∧ Nat.Prime q ∧ 4 * 10 ^ 18 + 2 = p + q := by
  sorry

end WeakGoldbach

Source

Boundary value needed by the prime-ladder reduction in Helfgott–Platt, arXiv:1305.3062v2 §4; explicit witness

653 + 3{,}999{,}999{,}999{,}999{,}999{,}349

View graph

4⋅1018+24\cdot 10^{18} + 24⋅1018+2 is a sum of two primes

$4\cdot 10^{18} + 2$ is a sum of two primes