Prime-power correction is small for $m > 2\cdot 10^{18}$

Proved

WeakGoldbach.prime_power_part_le_above_2e18

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

circle-methodgoldbachnumber-theoryprimes

For every natural number $m > 2\cdot 10^{18}$ , the part of the weighted symmetric-offset sum coming from offsets where at least one of $m-t$ , $m+t$ is a proper prime power (rather than prime) satisfies

\sum_{\substack{0 \le t \le m-2 \\ \text{not both prime}}} \Lambda(m-t)\,\Lambda(m+t) \;\le\; \tfrac{1}{10}\,\mathfrak{S}(2m)\,m.

This is elementary: proper prime powers below $2m$ number $O(\sqrt m \log_2 m)$ and each term is at most $\log^2(2m)$ , so the sum is $O(\sqrt m\,\mathrm{polylog}\, m)$ — dwarfed by the linear main term. It is the standard ``remove the prime powers'' step that passes from the weighted circle-method count to the genuine prime-pair count.

Preamble

import Mathlib

Formal statement

namespace WeakGoldbach

theorem prime_power_part_le_above_2e18 (m : ℕ) (hm : 2 * 10 ^ 18 < m) :
    ∑ t ∈ (Finset.range (m - 1)).filter
        (fun t => ¬ (Nat.Prime (m - t) ∧ Nat.Prime (m + t))),
      (ArithmeticFunction.vonMangoldt (m - t) : ℝ)
        * (ArithmeticFunction.vonMangoldt (m + t) : ℝ)
      ≤ (∏ p ∈ (2 * m).primeFactors.filter (2 < ·), ((p : ℝ) - 1) / ((p : ℝ) - 2))
          * (m : ℝ) * (1 / 10) := by
  sorry

end WeakGoldbach

Source

Standard elementary estimate; Vaughan, The Hardy-Littlewood Method

View graph

Prime-power correction is small for m>2⋅1018m > 2\cdot 10^{18}m>2⋅1018

Prime-power correction is small for $m > 2\cdot 10^{18}$