### Abstract

This article provides a short proof of the Prime Number Theorem in several equivalent forms, most notably π(x) ~ x/ln x where π(x) is the number of primes no larger than x. It also defines other basic number-theoretic functions related to primes like Chebyshev's functions ϑ and ψ and the “n-th prime number” function pn. We also show various bounds and relationship between these functions are shown. Lastly, we derive Mertens' First and Second Theorem, i. e. ∑p≤x ln p/p = ln x + O(1) and ∑p≤x 1/p = ln ln x + M + O(1/ln x). We also give explicit bounds for the remainder terms.

The proof of the Prime Number Theorem builds on a library of Dirichlet series and analytic combinatorics. We essentially follow the presentation by Newman. The core part of the proof is a Tauberian theorem for Dirichlet series, which is proven using complex analysis and then used to strengthen Mertens' First Theorem to ∑p≤x ln p/p = ln x + c + o(1).

A variant of this proof has been formalised before by Harrison in HOL Light, and formalisations of Selberg's elementary proof exist both by Avigad et al. in Isabelle and by Carneiro in Metamath. The advantage of the analytic proof is that, while it requires more powerful mathematical tools, it is considerably shorter and clearer. This article attempts to provide a short and clear formalisation of all components of that proof using the full range of mathematical machinery available in Isabelle, staying as close as possible to Newman's simple paper proof.

### License

BSD License

### Topics

- Mathematics/Number theory

### Session Prime_Number_Theorem

- Prime_Number_Theorem_Library
- Newman_Ingham_Tauberian
- Prime_Counting_Functions
- Prime_Number_Theorem
- Mertens_Theorems

### Depends on

- Stirling’s formula
- The Hurwitz and Riemann ζ Functions

### Used by

- Prime Number Theorem with Remainder Term
- The Irrationality of ζ(3)
- The Transcendence of Certain Infinite Series
- Elementary Facts About the Distribution of Primes

### Auto-related entries

- Prime Number Theorem with Remainder Term
- Elementary Facts About the Distribution of Primes
- Dirichlet Series

## Cite

×

Prime_Number_Theorem-AFP

    @article{Prime_Number_Theorem-AFP,
      author  = {Manuel Eberl and Lawrence C. Paulson},
      title   = {The Prime Number Theorem},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Prime_Number_Theorem.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Sep 20, 2018 : Isabelle2018