Main-term bound on the binary Goldbach integral, $m > 2\cdot10^{18}$

Open

WeakGoldbach.integral_main_term_above_2e18

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

circle-methodgoldbachnumber-theoryopen-problem

For an integer $m>2\cdot10^{18}$ , put

F(2m)=\prod_{\substack{p\mid2m\\p>2}}\frac{p-1}{p-2},\qquad S(\alpha,N)=\sum_{n<N}\Lambda(n)e(\alpha n).

The proposed estimate is

\operatorname{Re}\int_0^1 S(\alpha,2m)^2 e(-2m\alpha)\,d\alpha\ge\frac52 F(2m)m.

This is an OPEN quantitative sufficient condition for the strong-Goldbach tail, not an established analytic estimate or an equivalent formulation of mere prime-pair existence. The exact identity is $R(2m)=2W_m-\Lambda(m)^2$ , where $W_m=\sum_{t<m-1}\Lambda(m-t)\Lambda(m+t)$ . Thus the displayed estimate implies $W_m\ge(5/4)F(2m)m$ ; the reverse implication does not follow without accounting for the diagonal term.

The standard binary singular series is $\mathfrak S_2(2m)=2C_2F(2m)$ , with $C_2=\prod_{p>2}(1-(p-1)^{-2})$ . The Hardy-Littlewood prediction in this normalization is $R(2m)\sim4C_2F(2m)m$ , not $F(2m)m$ . That prediction does not establish the specific finite-threshold inequality above.

For existence alone, the proved prime-power correction bound $P_m\le F(2m)m/10$ already makes the strictly weaker inequality $R(2m)>F(2m)m/5$ sufficient. Effective major-arc errors and a sufficiently strong signed minor-arc lower bound must still be supplied; the global Parseval bound alone does not provide them.

Preamble

import Mathlib
import Definitions.Def_Vino_primes
import Definitions.Def_CircleMethod_char

Formal statement

namespace WeakGoldbach

theorem integral_main_term_above_2e18 (m : ℕ) (hm : 2 * 10 ^ 18 < m) :
    ((∫ α in (0:ℝ)..1, (Vino.vmSum α (2*m))^2
        * CircleMethod.e (-((2*m : ℕ) : ℝ) * α)).re : ℝ)
      ≥ (5 / 2 : ℝ)
        * (∏ p ∈ (2 * m).primeFactors.filter (2 < ·),
            ((p : ℝ) - 1) / ((p : ℝ) - 2)) * m := by
  sorry

end WeakGoldbach

Source

Original unproved finite-threshold sufficient estimate. Normalization reference: J. Pintz, A new explicit formula in the additive theory of primes with applications II. The exceptional set in Goldbach's problem, arXiv:1804.09084, Section 2, equation (2.9), https://ar5iv.labs.arxiv.org/html/1804.09084 . This reference does not assert or prove the displayed explicit-threshold estimate.

View graph

Main-term bound on the binary Goldbach integral, m>2⋅1018m > 2\cdot10^{18}m>2⋅1018

Main-term bound on the binary Goldbach integral, $m > 2\cdot10^{18}$