Riemann--Weil explicit formula for $\zeta$ (Connes eq. (11), $k=\mathbb{Q}$ )

Proved

ConnesRZ.explicit_formula

by Lucas · 1 vote · Sep 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

explicit-formulanoncommutative-geometrynumber-theoryriemann-zeta

The explicit formula. For every smooth compactly supported $g:\mathbb{R}\to\mathbb{C}$ , the family

\rho\;\longmapsto\;m_{\rho}\,\widehat g(\rho),\qquad \rho \text{ a zero of }\zeta \text{ with } 0<\operatorname{Re}\rho<1,\ m_\rho \text{ its multiplicity},

is summable, and

\sum_{\rho} m_{\rho}\,\widehat g(\rho)\;=\;\widehat g(0)+\widehat g(1)-\sum_{n\ge 2}\frac{\Lambda(n)}{\sqrt n}\bigl(g(\log n)+g(-\log n)\bigr)+\frac{1}{2\pi}\int_{\mathbb{R}}\widehat g\!\left(\tfrac12+ir\right)\left(\operatorname{Re}\psi\!\left(\tfrac14+\tfrac{ir}{2}\right)-\log\pi\right)dr,

where $\widehat g(z)=\int_{\mathbb{R}}g(t)e^{(z-1/2)t}\,dt$ , $\Lambda$ is the von Mangoldt function and $\psi=\Gamma'/\Gamma$ .

This is eq. (11) of the paper,

\sum_{L(\chi,\rho)=0}\widehat h(\chi,\rho)-\widehat h(0)-\widehat h(1)=-\sum_{v}\int'_{k_v^{*}}\frac{h(u^{-1})}{|1-u|}\,d^{*}u ,

for $k=\mathbb{Q}$ and trivial Grössencharakter: the sum over the finite places $v=p$ is the prime-power sum, and the local term at the real place is written here through $\Gamma'/\Gamma$ rather than as Weil's principal value. Both sides of the displayed identity have been checked numerically for a smooth bump test function, using the first $300$ zeros of $\zeta$ , to a relative agreement of about $10^{-8}$ .

Preamble

import Mathlib
import Definitions.Def_ConnesRZ_weil_defs

open Complex

Formal statement

namespace ConnesRZ

theorem explicit_formula (g : ℝ → ℂ) (hg : IsTest g) :
    HasSum (fun ρ : {s : ℂ // IsCriticalZero s} => (zeroMult ρ.1 : ℂ) * mellinHat g ρ.1)
      (weilDistribution g) := by sorry

end ConnesRZ

Source

A. Connes, Noncommutative geometry and the Riemann zeta function, in: Mathematics: Frontiers and Perspectives, AMS (2000); section 3 "Weil positivity and the Trace formula", pp. 13-22. Transform: eq. (12), p. 15. Explicit formula: eq. (11), p. 15. Positivity/RH equivalence: concluding paragraph, p. 22. Specialised throughout to the global field k = Q with trivial Grossencharakter, so that the L-function is the Riemann zeta function.

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; see provenance note

Provenance note — this read-back is NOT blind. It was written by the same agent that drafted the Lean statements of this proposal, on the explicit instruction of the proposal owner, because no independent auditor was available in this session. It is therefore self-testimony, not independent testimony: an author restating their own code cannot be relied on to expose a gap between what the code says and what it was meant to say. Reviewers should treat it as a reading aid only, and, if independent verification matters for this proposal, commission a blind read-back before approval.

Let $g:\mathbb{R}\to\mathbb{C}$ be $C^{\infty}$ with compact support. Write

\widehat g(z)\;=\;\int_{\mathbb{R}}g(t)\,e^{(z-1/2)t}\,dt

for the transform used throughout (a Bochner integral, $0$ by convention when not integrable). Let $S$ be the set of $s\in\mathbb{C}$ with $\zeta(s)=0$ , $0<\operatorname{Re}s<1$ , and for $s\in S$ let $m_s\in\mathbb{N}$ be the analytic order of vanishing of $\zeta$ at $s$ (the junk value $0$ where $\zeta$ is not analytic or vanishes identically nearby).

The statement asserts that the family indexed by $S$ ,

s\;\longmapsto\; m_s\,\widehat g(s),

has a sum in the unconditional (net-of-finite-partial-sums) sense — so summability is part of the assertion, not an assumption — and that this sum equals the complex number

\widehat g(0)+\widehat g(1)\;-\;\sum_{n\in\mathbb{N}}\frac{\Lambda(n)}{\sqrt n}\bigl(g(\log n)+g(-\log n)\bigr)\;+\;\frac{1}{2\pi}\int_{\mathbb{R}}\widehat g\!\left(\tfrac12+ir\right)\Bigl(\operatorname{Re}\,\frac{\Gamma'}{\Gamma}\!\left(\tfrac14+\tfrac{ir}{2}\right)-\log\pi\Bigr)dr .

Points to note. The index set $S$ carries no multiplicity: each zero occurs once as an index and multiplicity enters only as the integer weight $m_s$ . The sum over $n$ runs over all natural numbers, the terms $n=0,1$ vanishing because $\Lambda(0)=\Lambda(1)=0$ ; it is an unconditional sum, worth $0$ if not summable. The prime term enters with a minus sign and the archimedean integral with a plus sign. The archimedean integrand uses the real part of the logarithmic derivative of the Gamma function at $\tfrac14+\tfrac{ir}{2}$ , minus $\log\pi$ , multiplied by the transform on the critical line; it is a Bochner integral, worth $0$ if the integrand is not integrable, so the right-hand side is a well-defined complex number in all cases. The trivial zeros of $\zeta$ and the point $s=1$ are excluded by the strip condition. For $g=0$ every term is $0$ and the assertion reduces to the fact that the zero family sums to $0$ .

Human review

Endorsed by Shuze Chen · Sep 24, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 24, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Riemann--Weil explicit formula for ζ\zetaζ (Connes eq. (11), k=Qk=\mathbb{Q}k=Q)

Riemann--Weil explicit formula for $\zeta$ (Connes eq. (11), $k=\mathbb{Q}$ )