A formally verified proof of the prime number theorem

Jeremy Avigad; Kevin Donnelly; David Gray; Paul Raff

doi:10.1145/1297658.1297660

A formally verified proof of the prime number theorem

Jeremy Avigad
, Kevin Donnelly
, David Gray
, Paul Raff

Philosophy

Carnegie Mellon University
Boston University
Rutgers - The State University of New Jersey, New Brunswick

Research output: Contribution to journal › Article › peer-review

48 Scopus citations

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

Original language	English
Article number	2
Journal	ACM Transactions on Computational Logic
Volume	9
Issue number	1
DOIs	https://doi.org/10.1145/1297658.1297660
State	Published - Dec 1 2007

Keywords

Formal verification
Prime number theorem

Access to Document

10.1145/1297658.1297660

Cite this

@article{f72f4d9451a64a7f951c941909bd3603,

title = "A formally verified proof of the prime number theorem",

abstract = "The prime number theorem, established by Hadamard and de la Vall{\'e}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{\"o}s in 1948. We describe a formally verified version of Selberg's proof, obtained using the Isabelle proof assistant.",

keywords = "Formal verification, Prime number theorem",

author = "Jeremy Avigad and Kevin Donnelly and David Gray and Paul Raff",

year = "2007",

month = dec,

day = "1",

doi = "10.1145/1297658.1297660",

language = "English",

volume = "9",

journal = "ACM Transactions on Computational Logic",

issn = "1529-3785",

publisher = "Association for Computing Machinery ",

number = "1",

}

TY - JOUR

T1 - A formally verified proof of the prime number theorem

AU - Avigad, Jeremy

AU - Donnelly, Kevin

AU - Gray, David

AU - Raff, Paul

PY - 2007/12/1

Y1 - 2007/12/1

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

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

KW - Formal verification

KW - Prime number theorem

UR - https://www.scopus.com/pages/publications/37049032802

U2 - 10.1145/1297658.1297660

DO - 10.1145/1297658.1297660

M3 - Article

AN - SCOPUS:37049032802

SN - 1529-3785

VL - 9

JO - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

IS - 1

M1 - 2

ER -

A formally verified proof of the prime number theorem

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this