Under Lindelöf: $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. Assume the Lindelöf hypothesis: $\zeta(\tfrac12+it)=O(t^{\varepsilon})$ as $t\to+\infty$ for every $\varepsilon>0$. Then

This is the improvement of the error term in the Riemann–von Mangoldt formula from $O(\log T)$ to $o(\log T)$ conditional on the Lindelöf hypothesis.

Formalization Note The hypothesis is LindelofHypothesis and $N(T)$ is zetaZeroCount T, both from Definitions.Def_RiemannVonMangoldt_ZeroCounts; $o(\log T)$ is Mathlib's Asymptotics.IsLittleO along Filter.atTop.