A Formally Verified Proof of the Prime Number Theorem

ACM Transactions on Computational Logic 9 (1) (2007)
  Copy   BIBTEX

Abstract

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 Erdos in 1948. We describe a formally verified version of Selberg's proof, obtained using the Isabelle proof assistant

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 74,569

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2010-09-14

Downloads
49 (#237,328)

6 months
1 (#418,511)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

David Emmanuel Gray
State University of New York, Buffalo
Jeremy Avigad
Carnegie Mellon University

Citations of this work

Maddy On The Multiverse.Claudio Ternullo - 2019 - In Deniz Sarikaya, Deborah Kant & Stefania Centrone (eds.), Reflections on the Foundations of Mathematics. Berlin: Springer Verlag. pp. 43-78.
Understanding, Formal Verification, and the Philosophy of Mathematics.Jeremy Avigad - 2010 - Journal of the Indian Council of Philosophical Research 27:161-197.

View all 6 citations / Add more citations

References found in this work

No references found.

Add more references