# A formally verified proof of the prime number theorem

@article{Avigad2007AFV, title={A formally verified proof of the prime number theorem}, author={Jeremy Avigad and Kevin Donnelly and David Gray and Paul Raff}, journal={ACM Trans. Comput. Log.}, year={2007}, volume={9}, pages={2} }

The prime number theorem, established by Hadamard and de la Vallée Poussin independently in 1896, asserts that the density of primes in the positive integers is asymptotic to 1/ln x. Whereas their proofs made serious use of the methods of complex analysis, elementary proofs were provided by Selberg and Erdös in 1948. We describe a formally verified version of Selberg's proof, obtained using the Isabelle proof assistant.

#### Topics from this paper

#### Paper Mentions

#### 92 Citations

Formalizing an Analytic Proof of the Prime Number Theorem

- Computer Science
- Journal of Automated Reasoning
- 2009

This work describes the computer formalization of a complex-analytic proof of the Prime Number Theorem (PNT), a classic result from number theory characterizing the asymptotic density of the primes, and analyzes the relationship between the formal proof and its informal counterpart. Expand

A formalized proof of Dirichlet's theorem on primes in arithmetic progression

- Computer Science
- J. Formaliz. Reason.
- 2009

A simple and efficient proof of the Dirichlet's theorem informally, which is otherwise difficult to find in one self-contained place at an elementary level, is described. Expand

A Formally Verified Proof of the Central Limit Theorem

- Computer Science, Mathematics
- Journal of Automated Reasoning
- 2017

The proof of the Central Limit Theorem uses characteristic functions, which are a kind of Fourier transform, to demonstrate that, under suitable hypotheses, sums of random variables converge weakly to the standard normal distribution. Expand

Formalization of the prime number theorem and Dirichlet's theorem

- Mathematics, Computer Science
- FM4M/MathUI/ThEdu/DP/WIP@CIKM
- 2016

The formalization of Dirichlet's theorem on the infinitude of primes in arithmetic progressions is presented, and Selberg's elementary proof of the prime number theorem is presented within the proof system Metamath. Expand

A proof of Bertrand's postulate

- Mathematics, Computer Science
- J. Formaliz. Reason.
- 2012

We discuss the formalization, in the Matita Interactive Theorem Prover, of some results by Chebyshev concerning the distribution of prime numbers, subsuming, as a corollary, Bertrand's postulate. … Expand

A Formal Proof of the Irrationality of ζ(3)

- Computer Science, Mathematics
- Log. Methods Comput. Sci.
- 2021

This paper presents a complete formal verification of a proof that the evaluation of the Riemann zeta function at 3 is irrational, using the Coq proof assistant, and establishes that some sequences satisfy a common recurrence. Expand

A formal proof of Hensel's lemma over the p-adic integers

- Mathematics, Computer Science
- CPP
- 2019

Hensel’s lemma, described by Gouvêa as the “most important algebraic property of the p-adic numbers,” shows the existence of roots of polynomials over ℚp provided an initial seed point, and the theorem can be proved for thep-adics with significantly weaker hypotheses than for general rings. Expand

About the Formalization of Some Results by Chebyshev in Number Theory

- Computer Science
- TYPES
- 2008

We discuss the formalization, in the Matita Interactive Theorem Prover, of a famous result by Chebyshev concerning the distribution of prime numbers, essentially subsuming, as a corollary, Bertrand's… Expand

A Mechanized Proof of the Basic Perturbation Lemma

- Mathematics, Computer Science
- Journal of Automated Reasoning
- 2007

A complete mechanized proof of the result in homological algebra known as basic perturbation lemma is presented, carried out in the proof assistant Isabelle in the implementation of higher-order logic (HOL) available in the system. Expand

The Prime Number Theorem

- Computer Science, Mathematics
- Arch. Formal Proofs
- 2018

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. Expand

#### References

SHOWING 1-10 OF 36 REFERENCES

The Prime Number Theorem

- 2001

The Prime Number Theorem asserts that the number of primes less than or equal to x is approximately equal to x log x for large values of x (here and for the rest of these notes, log denotes the… Expand

Notes on a Formalization of the Prime Number Theorem

- Mathematics
- 2004

The system thereby confirmed that the prime number theorem is a consequence of the axioms of higher-order logic together with an axiom asserting the existence of an infinite set. All told, our number… Expand

The prime number theorem and fragments ofP A

- Mathematics, Computer Science
- Arch. Math. Log.
- 1994

SummaryWe show that versions of the prime number theorem as well as equivalent statements hold in an arbitrary model ofIΔ0+exp.

Number theory and elementary arithmetic

- Mathematics
- 2003

Elementary arithmetic (also known as “elementary function arithmetic”) is a fragment of first-order arithmetic so weak that it cannot prove the totality of an iterated exponential function.… Expand

Elementary Methods in Number Theory

- Mathematics
- 1999

Elementary Methods in Number Theory begins with "a first course in number theory" for students with no previous knowledge of the subject. The main topics are divisibility, prime numbers, and… Expand

A Proof-Producing Decision Procedure for Real Arithmetic

- Computer Science, Mathematics
- CADE
- 2005

This is the first generally useful proof-producing implementation of a quantifier elimination procedure for real closed fields, and convincing examples of its value in interactive theorem proving are demonstrated. Expand

Isabelle/HOL: A Proof Assistant for Higher-Order Logic

- Mathematics
- 2002

Elementary Techniques.- 1. The Basics.- 2. Functional Programming in HOL.- 3. More Functional Programming.- 4. Presenting Theories.- Logic and Sets.- 5. The Rules of the Game.- 6. Sets, Functions,… Expand

An Introduction to the Theory of Numbers

- Mathematics, Philosophy
- 1938

This is the fifth edition of a work (first published in 1938) which has become the standard introduction to the subject. The book has grown out of lectures delivered by the authors at Oxford,… Expand

Introduction to analytic number theory

- Mathematics
- 1976

This is the first volume of a two-volume textbook which evolved from a course (Mathematics 160) offered at the California Institute of Technology during the last 25 years. It provides an introduction… Expand

An Introduction to the Theory of Numbers

- Nature
- 1946

THIS book must be welcomed most warmly into X the select class of Oxford books on pure mathematics which have reached a second edition. It obviously appeals to a large class of mathematical readers.… Expand