The three primes counting identity

Proved

Vino.three_primes_count

by tabbott · Sep 2, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analytic-number-theorycircle-methodnumber-theoryprime-numbers

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)^3\,e(-n\alpha)\,d\alpha\;=\;\sum_{\substack{n_1+n_2+n_3=n\\ n_1,n_2,n_3<N}}\Lambda(n_1)\Lambda(n_2)\Lambda(n_3)=:R(n).

This is the starting point of the three primes theorem. The quantity $R(n)$ is the von Mangoldt weighted count of representations of $n$ as an ordered sum of three prime powers below $N$ ; showing $R(n)>0$ for large odd $n$ is exactly what Vinogradov's theorem asserts, and the circle method attacks it by splitting the integral into major and minor arcs.

The identity itself is exact and elementary — no estimate is involved — but it is the bridge that turns an additive question about primes into an analytic question about the size of $S(\alpha,N)$ on the circle.

Preamble

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

Formal statement

namespace Vino

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

end Vino

Source

R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997, Section 1.1 equation (1.4) (the fundamental counting identity of the circle method) and Chapter 3 (the three primes theorem).

View graph