Positivity of the Weil distribution implies the Riemann hypothesis

Proved

ConnesRZ.weil_positivity_implies_RH

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

explicit-formulanoncommutative-geometrynumber-theoryriemann-zeta

Goal of the mission. Suppose the Weil distribution is positive, i.e. for every smooth compactly supported $g:\mathbb{R}\to\mathbb{C}$ ,

\operatorname{Re}\,W\bigl(g\star g^{*}\bigr)\;\ge\;0 ,

where $W$ is the Weil distribution of the mission's definition bundle and $g^{*}(t)=\overline{g(-t)}$ . Then the Riemann hypothesis holds: every zero $\rho$ of $\zeta$ with $0<\operatorname{Re}\rho<1$ satisfies $\operatorname{Re}\rho=\tfrac12$ .

This is the direction of the equivalence asserted on p. 22 of the paper that produces RH, for $k=\mathbb{Q}$ with trivial Grössencharakter: Connes' chain is "trace formula $\Rightarrow$ positivity of the Weil distribution $\Rightarrow$ RH", and this statement is its last link. The intended route is the explicit formula, which turns $W(g\star g^{*})$ into the sum over the zeros of $m_\rho\,\widehat g(\rho)\overline{\widehat g(1-\bar\rho)}$ ; a zero off the critical line comes with its mirror zero $1-\bar\rho$ , and a suitable family of test functions makes that pair contribute negatively, contradicting the hypothesis.

Preamble

import Mathlib
import Definitions.Def_ConnesRZ_weil_defs

open Complex

Formal statement

namespace ConnesRZ

theorem weil_positivity_implies_RH
    (hpos : ∀ g : ℝ → ℂ, IsTest g → 0 ≤ (weilDistribution (conv g (starInv g))).re) :
    ∀ s : ℂ, IsCriticalZero s → s.re = 1 / 2 := 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.

The statement has one hypothesis and one conclusion, and mentions no zeros in the hypothesis and no test functions in the conclusion.

Hypothesis. For every function $g:\mathbb{R}\to\mathbb{C}$ that is $C^{\infty}$ with compact support, the real part of

W\bigl(g\star g^{*}\bigr)=\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

is $\ge 0$ , where $G(t)=\int_{\mathbb{R}}g(s)\overline{g(s-t)}\,ds$ and $\widehat G(z)=\int_{\mathbb{R}}G(t)e^{(z-1/2)t}dt$ , all integrals being Bochner integrals and the sum an unconditional sum, each equal to the junk value $0$ when integrability or summability fails. Only the real part is constrained.

Conclusion. For every $s\in\mathbb{C}$ : if $\zeta(s)=0$ and $0<\operatorname{Re}s<1$ , then $\operatorname{Re}s=\tfrac12$ . This is the Riemann hypothesis for Mathlib's riemannZeta, stated for the open strip only; it says nothing about the trivial zeros or about possible zeros with $\operatorname{Re}s\in\{0,1\}$ .

The implication is asserted in this direction only. The hypothesis quantifies over a class that is nonempty (smooth compactly supported bump functions exist), so the statement is not vacuous on that account; whether the hypothesis is satisfiable is exactly what is at issue, and if the hypothesis were unsatisfiable the theorem would be provable without touching the zeta function. Nothing in the statement asserts that the quantity $W(g\star g^{*})$ is real, or that the sum over the zeros of $\zeta$ converges, or any relation between $W$ and the zeros: the link between the two sides is not part of this statement.

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).
Endorsed by waitingintime · Oct 9, 2026
Confirmed by the mission captain (proposal self-audit).

View graph