### Abstract

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.

### License

BSD License

### Topics

- Mathematics/Number theory

### Related publications

- The Theory of the Riemann Zeta-Function, E. C. Titchmarsh, D. R. Heath-Brown
- The Theory of Functions, E. C. Titchmarsh
- Perron's Formula and the Prime Number Theorem for Automorphic L-Functions, Jianya Liu, Y. Ye
- The distribution of prime numbers, A. E. Ingham

### Session PNT_with_Remainder

- PNT_Notation
- PNT_Remainder_Library
- Relation_of_PNTs
- PNT_Complex_Analysis_Lemmas
- Zeta_Zerofree
- PNT_Subsummable
- Perron_Formula
- PNT_with_Remainder

### Depends on

- The Prime Number Theorem

### Auto-related entries

- Elementary Facts About the Distribution of Primes
- Dirichlet Series
- Pell’s Equation
- Treaps
- Bernoulli Numbers

## Cite

×

PNT_with_Remainder-AFP

    @article{PNT_with_Remainder-AFP,
      author  = {Shuhao Song and Bowen Yao},
      title   = {Prime Number Theorem with Remainder Term},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2024},
      note    = {\url{https://isa-afp.org/entries/PNT_with_Remainder.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest