The two primes counting identity

Proved

Vino.two_primes_count

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

analytic-number-theorycircle-methodgoldbachnumber-theoryprimes

Let $S(\alpha,N)=\sum_{n<N}\Lambda(n)e(\alpha n)$ be the von Mangoldt exponential sum. Then for every $n$ ,

\int_0^1 S(\alpha,N)^2\,e(-n\alpha)\,d\alpha\;=\;\sum_{\substack{a+b=n\\ a,b<N}}\Lambda(a)\Lambda(b).

This is the starting point of the circle-method attack on the binary Goldbach conjecture: the right-hand side is the weighted count of representations of $n$ as an ordered sum of two prime powers below $N$ , and positivity of this weighted count (after stripping the proper prime powers, which contribute $O(\sqrt n\,\mathrm{polylog}\, n)$ ) is exactly what a proof of Goldbach must produce. The identity itself is exact and elementary — it is orthogonality of the additive characters $e(k\alpha)$ on $[0,1]$ — and it is the binary analog of Vino.three_primes_count.

Preamble

import Definitions.Def_Vino_primes
import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
open Finset

Formal statement

namespace Vino

theorem two_primes_count (N n : ℕ) :
    (∫ α in (0:ℝ)..1, (vmSum α N) ^ 2 * CircleMethod.e (-(n : ℝ) * α))
      = ∑ a ∈ Finset.range N, ∑ b ∈ Finset.range N,
          if a + b = n then
            ((ArithmeticFunction.vonMangoldt a : ℝ) : ℂ)
              * ((ArithmeticFunction.vonMangoldt b : ℝ) : ℂ)
          else 0 := by
  sorry

end Vino

Source

R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Section 1.1 (the fundamental counting identity), specialised to two summands

View graph