Motivation

The Riemann hypothesis (RH) asserts that every zero of the Riemann zeta function $\zeta$ in the strip $0 < \operatorname{Re} s < 1$ has $\operatorname{Re} s = \tfrac12$. One of the few reformulations that turns RH into a positivity statement, rather than a statement about the location of points, goes back to A. Weil (1952): the explicit formula expresses a sum over the zeros of $\zeta$ as a sum of local contributions over the places of $\mathbb{Q}$, and RH is equivalent to the resulting functional being positive on elements of the form $g \star g^{*}$.

Connes' 1999 programme paper Noncommutative geometry and the Riemann zeta function takes this reformulation as its endpoint. It builds a geometric framework — the adele class space $X = \mathbb{A}/k^{*}$ carrying an action of the idele class group $C_k$ — in which the explicit formula appears as a Lefschetz formula, the zeros of $L$-functions appear spectrally, and the paper's concluding assertion (§3, p. 22) is that the validity of the global trace formula implies, and is in fact equivalent to, positivity of the Weil distribution, i.e. RH for all $L$-functions with Grössencharakter.

This mission formalizes the arithmetic core of that endpoint in its simplest instance: the global field $k = \mathbb{Q}$ with trivial Grössencharakter, so that the $L$-function is $\zeta$ itself. Concretely it asks for (i) the Riemann–Weil explicit formula for $\zeta$ in the shape of Connes' equation (11), and (ii) both directions of the equivalence between positivity of the resulting Weil distribution and RH.

A rough timeline of the statements involved: Riemann (1859) gave the first explicit formula; von Mangoldt (1895) proved it rigorously; Weil (Sur les "formules explicites" de la théorie des nombres premiers, 1952) extended it to all global fields and isolated the positivity criterion; Bombieri (Remarks on Weil's quadratic functional in the theory of prime numbers, 2000) studied the associated quadratic functional in detail; Connes (1996–1999) gave the trace-formula interpretation formalized in part here.

Setting

All objects live on the group $\mathbb{R}^{*}_{+}$, the module of the idele class group of $\mathbb{Q}$, written additively through $u = e^{t}$, $d^{*}u = dt$.

A test function is a map $g : \mathbb{R} \to \mathbb{C}$ that is $C^{\infty}$ and has compact support (IsTest).

Its transform is

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

which is Connes' $\widehat h(z) = \int_{C_k} h(u)\,|u|^{z}\,d^{*}u$ in the coordinate $u = e^{t}$, shifted by $\tfrac12$ so that $z$ is the variable of $\zeta$ (mellinHat). On the critical line, $\widehat{g}(\tfrac12 + i r) = \int_{\mathbb{R}} g(t) e^{irt}\,dt$ is the ordinary Fourier transform.

The involution is $g^{*}(t) = \overline{g(-t)}$, i.e. $h^{*}(u) = \overline{h(u^{-1})}$ (starInv), and convolution is $(g_1 \star g_2)(t) = \int_{\mathbb{R}} g_1(s)\, g_2(t-s)\, ds$ (conv).

The Weil distribution of a test function $g$ collects the pole terms, the finite places and the archimedean place:

$$W(g) \;=\; \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)\Bigl(\operatorname{Re}\psi\left(\tfrac14 + \tfrac{ir}{2}\right) - \log \pi\Bigr) dr ,$$

where $\Lambda$ is the von Mangoldt function and $\psi = \Gamma'/\Gamma$ (weilDistribution, with the three pieces named mellinHat, primeSum, archTerm). The middle sum is Weil's contribution of the finite places $v = p$, the last integral the contribution of the real place.

The spectral side is

$$Z(g) \;=\; \sum_{\rho} m_{\rho}\, \widehat{g}(\rho),$$

the sum over the zeros $\rho$ of $\zeta$ with $0 < \operatorname{Re}\rho < 1$, each counted with its multiplicity $m_\rho$ (zeroSum, IsCriticalZero, zeroMult).

Formalization targets

Goal — positivity of the Weil distribution implies RH

$$\Bigl(\forall\, g \text{ test}:\; \operatorname{Re} W\bigl(g \star g^{*}\bigr) \ge 0\Bigr) \;\Longrightarrow\; \bigl(\forall \rho,\ \zeta(\rho) = 0,\ 0 < \operatorname{Re}\rho < 1 \;\Rightarrow\; \operatorname{Re}\rho = \tfrac12\bigr).$$

This is the direction that yields RH, and it is the weakest form of the endpoint of the paper: it fixes no rate, no test-function normalization beyond $C_c^{\infty}$, and no numerical constant.

Milestone — the explicit formula (Connes (11))

$$\sum_{\rho} m_\rho\,\widehat g(\rho) \;=\; W(g) \qquad \text{for every test function } g,$$

with the sum over zeros asserted to be (unconditionally) summable.

Milestone — the converse direction

$$\text{RH} \;\Longrightarrow\; \forall\, g \text{ test}:\ \operatorname{Re} W\bigl(g \star g^{*}\bigr) \ge 0 .$$

Together with the goal this is the equivalence asserted on p. 22 of the paper, in the case $k = \mathbb{Q}$, trivial Grössencharakter.

Supporting statements

The $*$-identity $\widehat{g \star g^{*}}\left(\tfrac12 + ir\right) = \bigl|\widehat g\left(\tfrac12+ir\right)\bigr|^{2}$ on the critical line, and the fact that $g \star g^{*}$ is again a test function.

Significance

Weil's positivity criterion is one of the standard equivalent forms of RH, and the only one in which the arithmetic input (the primes, through $\Lambda$) and the archimedean input (the $\Gamma$-factor) enter as separate, explicitly computable local terms. Formalizing it produces a machine-checked bridge between the zeros of $\zeta$ and prime sums: the explicit formula milestone is the reusable object here, since essentially every analytic application of zeta zeros — zero-density estimates, prime-counting error terms, pair-correlation statistics — is an instance of it.

Status honesty: neither RH nor the positivity statement is known; the explicit formula and both implications relating positivity to RH are classical theorems, proved but not, as far as the catalog shows, formalized in Lean. Mathlib currently provides $\zeta$, its functional equation, the von Mangoldt function and $\Gamma$, but no explicit formula of any kind. What this mission adds on top of the paper is therefore the formal proof of known results, not new mathematics.

Difficulty

The obvious route to the explicit formula — integrate $-\zeta'/\zeta(s)\widehat g(s)$ over a vertical line, move the contour to the reflected line, collect residues — fails to be routine at exactly two points. First, moving the contour requires control of $\zeta'/\zeta$ on horizontal segments between zeros, which is where the classical proof invests most of its work; Mathlib has bounds near $\operatorname{Re} s = 1$ but nothing of this shape inside the strip. Second, the sum over zeros must be shown to converge unconditionally, which needs a zero-counting bound of Riemann–von Mangoldt type ($N(T) \ll T\log T$) that is not in Mathlib either.

For the goal implication, the naive idea — pick a test function whose transform is supported near a hypothetical off-line zero — is unavailable: $\widehat g$ is entire whenever $g$ has compact support, so it cannot be localized. The classical argument instead exploits the symmetry $\rho \mapsto 1-\bar\rho$ of the zero set and makes the off-line quadruple contribute a negative amount in the limit along a family of test functions.

Formalization scope

Conventions the Lean statements commit to. Test functions are $\mathbb{C}$-valued on $\mathbb{R}$, ContDiff ℝ (⊤ : ℕ∞) (so $C^{\infty}$, not analytic) with HasCompactSupport; the multiplicative group $\mathbb{R}^{*}_{+}$ is always written additively. The transform carries the $\tfrac12$-shift shown above, so the critical line is $\operatorname{Re} z = \tfrac12$ and $\widehat{g}(0), \widehat{g}(1)$ are the two pole terms. Zeros are indexed by the subtype $\{s : 0 < \operatorname{Re} s < 1,\ \zeta(s) = 0\}$ and weighted by (analyticOrderAt riemannZeta s).toNat; the trivial zeros are excluded. Integrals are Bochner integrals and sums are tsum, so both take the junk value $0$ when the integrand is not integrable or the family is not summable — for that reason the explicit formula is stated as a HasSum, which carries summability, rather than as an equation between tsums. The archimedean term is written with $\operatorname{Re}\psi$, $\psi =$ logDeriv Complex.Gamma, rather than as a principal value, to avoid a second regularization convention.

The goal is not trivially satisfiable: its hypothesis quantifies over a nonempty class (smooth bump functions exist), and its conclusion is RH for $\zeta$, so no vacuous reading is available.

Infrastructure a complete development needs, all reusable beyond this mission: growth bounds for $\zeta'/\zeta$ inside the critical strip, a Riemann–von Mangoldt zero-counting bound, Fourier analysis of $C^\infty_c$ functions (Paley–Wiener style decay of $\widehat g$), and the Hadamard product / functional equation package for the completed zeta function.

Out of scope, and deliberately so: Connes' operator-theoretic trace formula (equations (41) and (45) of the paper) and the spectral realization theorem of p. 17. Both are statements about traces of operators on Hilbert space, and Mathlib presently has no trace-class operator theory to state them faithfully. The mission therefore formalizes the arithmetic side of the paper's endpoint; contributions that build the missing operator theory, or that extend the statements from $\zeta$ to Dirichlet $L$-functions and Hecke $L$-functions with Grössencharakter, are welcome.

Selected references

• A. Connes, Noncommutative geometry and the Riemann zeta function, in Mathematics: Frontiers and Perspectives, AMS (2000) — the source of this mission (§3, equations (11) and (45), and the concluding assertion on p. 22).
• A. Connes, Trace formula in noncommutative geometry and the zeros of the Riemann zeta function, Selecta Math. (N.S.) 5 (1999) — reference [9] of the source. https://arxiv.org/abs/math/9811068
• A. Weil, Sur les "formules explicites" de la théorie des nombres premiers, Comm. Sém. Math. Univ. Lund (1952) — reference [27] of the source.
• E. Bombieri, Remarks on Weil's quadratic functional in the theory of prime numbers, I (2000).
• H. Iwaniec and E. Kowalski, Analytic Number Theory, AMS Colloquium Publications 53 (2004), Chapter 5 (explicit formulas).