Riemann Hypothesis
The first research project. Mathlib already *states* the claim as `RiemannHypothesis`. The tree below is the working map: landscape facts we inherit, equivalent formulations to prove, and the attack routes that have historically moved the needle. The closed term is still a `sorry`.
Riemann hypothesis
A closed Lean term of type RiemannHypothesis.
Which equivalent form or partial result is the shortest path to a new unconditional theorem about riemannZeta?
A positive proportion on the line
Selberg / Levinson / Conrey / Alpöge–Furman: more than two thirds of zeros are simple and on the critical line.
Can we formalize a proportion theorem, then ask what new arithmetic input would push the constant to 1?
Explicit formulae
Weil's dictionary: primes ↔ zeros, with test functions. Almost every modern approach speaks it.
What is the weakest test-function class for which we can prove an explicit formula sorry-free?
Weil positivity
RH iff the Weil pairing is positive semidefinite on a suitable space of test functions.
Can we define WeilPairing without opaque, then prove the iff?
Li's criterion
RH iff λₙ ≥ 0 for all n. A positivity statement, not a zero-location statement.
Define LiCoefficient from completedRiemannZeta and prove the iff.
Hilbert–Pólya
Zeros as eigenvalues of a self-adjoint operator. No such operator is constructed.
Is there an operator we can even write down?
Riemann hypothesis
Status: sorry
Every non-trivial zero of ζ has real part 1/2
Landscape of ζ
Status: library
What Mathlib already knows about ζ
Dirichlet series
Status: library
For Re(s) > 1, ζ(s) = Σ n⁻ˢ
Euler product
Status: library
For Re(s) > 1, ζ(s) = Π_p (1 − p⁻ˢ)⁻¹
Holomorphic off s = 1
Status: library
ζ is holomorphic on ℂ \ {1}
Functional equation
Status: library
ζ(1 − s) is an explicit multiple of ζ(s)
Trivial zeros
Status: library
ζ(−2n) = 0 for n = 1, 2, 3, …
No zeros on Re(s) ≥ 1
Status: library
If Re(s) ≥ 1 then ζ(s) ≠ 0
Zeros are discrete
Status: library
The zero set of ζ is discrete and closed
Equivalent formulations
Status: open
RH restated so a different tree might reach it
Li's criterion
Status: sorry
RH ⇔ λₙ ≥ 0 for all n ≥ 1
Weil positivity
Status: sorry
RH ⇔ the Weil pairing is positive semidefinite
Chebyshev error term
Status: sorry
RH ⇔ ψ(x) = x + O(x^{1/2+ε})
Attack routes
Status: open
Historical programmes that have moved zeros toward the line
Zero-free regions
Status: open
Classical regions to the left of Re = 1
Zero-density estimates
Status: open
Few zeros can stray far from the line
A positive proportion on the line
Status: open
liminf N₀(T)/N(T) ≥ 2/3 (and better)
Hilbert–Pólya
Status: open
Zeros as eigenvalues of a self-adjoint operator
Explicit formulae
Status: open
Primes ↔ zeros, with test functions