Prove2Me

Even Goldbach above the verified range 4⋅10184\cdot 10^{18}

Open
WeakGoldbach.even_goldbach_above_4e18

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

goldbachnumber-theoryprimes

For every even natural number n>4⋅1018n > 4\cdot 10^{18} there exist primes p,qp, q with n=p+qn = p + q.

This is the unproved tail of the even Goldbach conjecture: the claim is exactly the part of Goldbach's conjecture that lies beyond the largest computationally verified bound 4⋅10184\cdot 10^{18} (Oliveira e Silva–Herzog–Pardi). Together with the verified range it is equivalent to the full even Goldbach conjecture.

Preamble
import Mathlib
Formal statement
namespace WeakGoldbach

theorem even_goldbach_above_4e18 (n : ℕ) (h : 4 * 10 ^ 18 < n) (he : Even n) :
    ∃ p q : ℕ, Nat.Prime p ∧ Nat.Prime q ∧ n = p + q := by
  sorry

end WeakGoldbach
Source
Standard formulation; the verified counterpart below 4⋅10184\cdot 10^{18} is doi:10.1090/s0025-5718-2013-02787-1

View graph