Prove2Me

Under RH: N(T)=T2πlog⁡T2π−T2π+O(log⁡T/log⁡log⁡T)N(T)=\frac{T}{2\pi}\log\frac{T}{2\pi}-\frac{T}{2\pi}+O(\log T/\log\log T)

Open
RiemannVonMangoldt.riemann_hypothesis_error_bigO

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theoryriemann-zetazeros-of-zeta

Write N(T)N(T) for the number of zeros ρ\rho of the Riemann zeta function ζ(s)\zeta(s) with 0<Re⁡ρ<10<\operatorname{Re}\rho<1 and 0<Im⁡ρ≤T0<\operatorname{Im}\rho\le T, counted with multiplicity. Assume the Riemann hypothesis: every nontrivial zero of ζ\zeta has real part 12\tfrac12. Then

N(T)=T2πlog⁡T2π−T2π+O ⁣(log⁡Tlog⁡log⁡T)(T→∞).N(T)=\frac{T}{2\pi}\log\frac{T}{2\pi}-\frac{T}{2\pi}+O\!\left(\frac{\log T}{\log\log T}\right)\qquad (T\to\infty).

This is the conditional improvement of the error term in the Riemann–von Mangoldt formula under the Riemann hypothesis.

Formalization Note The hypothesis is Mathlib's RiemannHypothesis; N(T)N(T) is zetaZeroCount T; the OO is Asymptotics.IsBigO along Filter.atTop.

Preamble
import Mathlib
import Definitions.Def_RiemannVonMangoldt_ZeroCounts

open Filter Asymptotics Real
Formal statement
namespace RiemannVonMangoldt

theorem riemann_hypothesis_error_bigO (hRH : RiemannHypothesis) :
    (fun T : ℝ => zetaZeroCount T - (T / (2 * π) * Real.log (T / (2 * π)) - T / (2 * π)))
      =O[atTop] (fun T : ℝ => Real.log T / Real.log (Real.log T)) := by sorry

end RiemannVonMangoldt
Source
Wikipedia, "Riemann–von Mangoldt formula", revision oldid=1362774495 (https://en.wikipedia.org/w/index.php?title=Riemann–von_Mangoldt_formula&oldid=1362774495), paragraph "Under the Lindelöf and Riemann hypotheses, the error terms can be improved to o(log T) and O(log T / log log T) respectively" (second case). Titchmarsh (1986), Theorem 14.13.
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph