Prove2Me

Positive count of symmetric prime offsets around m>2⋅1018m > 2\cdot 10^{18}

Open
WeakGoldbach.symmetric_pair_count_pos_above_2e18

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

goldbachnumber-theoryprimes

For every natural number m>2⋅1018m > 2\cdot 10^{18}, the counting function

R(m)=#{t≤m−2:both m−t and m+t are prime}R(m) = \#\{t \le m - 2 : \text{both } m - t \text{ and } m + t \text{ are prime}\}

is positive. Since 2m=(m−t)+(m+t)2m = (m-t) + (m+t), this is the counting-function form of the even Goldbach conjecture — the quantity the circle method estimates, and the positivity claim that every attempted proof must establish.

Preamble
import Mathlib
Formal statement
namespace WeakGoldbach

theorem symmetric_pair_count_pos_above_2e18 (m : ℕ) (hm : 2 * 10 ^ 18 < m) :
    0 < ((Finset.range (m - 1)).filter
      (fun t => Nat.Prime (m - t) ∧ Nat.Prime (m + t))).card := by
  sorry

end WeakGoldbach
Source
Counting-function form of the Goldbach conjecture

View graph