Prove2Me

Montgomery–Vaughan: E(x)≪x1−δE(x) \ll x^{1-\delta}

Open
Goldbach.exceptional_set_power_saving

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

circle-methodexceptional-setgoldbachnumber-theoryprimes

The number E(x)E(x) of even integers 4≤n≤x4 \le n \le x that are not a sum of two primes satisfies E(x)≪x1−δE(x) \ll x^{1-\delta} for some absolute δ>0\delta > 0 and absolute constant CC.

This is the Montgomery–Vaughan exceptional-set theorem (1975): the circle method applied to binary Goldbach does prove the conjecture for almost all even numbers, since on major arcs the singular series is bounded below and the major-arc mass is correct; failures are confined to a power-saving exceptional set. The current best exponent is δ\delta near 1/21/2 (Pintz). A power-saving exceptional set can in principle contain an unbounded tail, so this does not yield even_goldbach_above_4e18\texttt{even\_goldbach\_above\_4e18}.

Preamble
import Mathlib
Formal statement
namespace Goldbach

theorem exceptional_set_power_saving :
    ∃ C δ : ℝ, 0 < δ ∧ ∀ x : ℝ, 1 ≤ x →
      ((Set.ncard {n : ℕ | 4 ≤ n ∧ n ≤ Nat.floor x ∧ Even n ∧
        ¬ ∃ p q : ℕ, Nat.Prime p ∧ Nat.Prime q ∧ n = p + q}) : ℝ)
        ≤ C * x ^ (1 - δ) := by
  sorry

end Goldbach
Source
H. L. Montgomery and R. C. Vaughan, The exceptional set in Goldbach's problem, Acta Arithmetica 27 (1975), 353-370

View graph