A Formally Verified Proof of the Prime Number Theorem
journal contributionposted on 01.01.2007 by Jeremy Avigad, Kevin Donnelly, David Gray, Paul Raff
Any type of content formally published in an academic journal, usually following a peer-review process.
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.