Riemann–von Mangoldt formula: $N(T)=\frac{T}{2\pi}\log\frac{T}{2\pi}-\frac{T}{2\pi}+O(\log T)$

Write $N(T)$ for the number of zeros $\rho$ of the Riemann zeta function $\zeta(s)$ with $0<\operatorname{Re}\rho<1$ and $0<\operatorname{Im}\rho\le T$, counted with multiplicity. The Riemann–von Mangoldt formula states that

that is, there are constants $C$ and $T_0$ such that $\bigl|N(T)-\frac{T}{2\pi}\log\frac{T}{2\pi}+\frac{T}{2\pi}\bigr|\le C\log T$ for all $T\ge T_0$.

The formula was stated by Riemann in 1859 and proved by von Mangoldt in 1905. It is the basic quantitative statement about the vertical distribution of the nontrivial zeros: the zeros up to height $T$ number about $\frac{T}{2\pi}\log T$, and their average spacing at height $T$ is about $2\pi/\log T$.

Formalization Note $N(T)$ is zetaZeroCount T from Definitions.Def_RiemannVonMangoldt_ZeroCounts; the $O(\log T)$ is Mathlib's Asymptotics.IsBigO along Filter.atTop.