Prime Number Theorem with Remainder Term

We have formalized the proof of the Prime Number Theorem with remainder term. This is the first formalized version of PNT with an explicit error term. There are many useful results in this AFP entry. First, the main result, prime number theorem with remainder: \[\pi(x) = \operatorname{Li}(x) + O\left(x \exp\left( -\sqrt{\log x}/3653 \right)\right)\] Second, the zero-free region of the Riemann zeta function: \[\zeta(\beta + i\gamma) \neq 0 \text{ when } \beta \ge 1 - \frac{1}{952320}\left(\log (|\gamma| + 2)\right)^{-1}\] Moreover, we proved a revised version of Perron's formula, together with the zero-free region we can prove the main result.