file.pdf (265.08 kB)
A Formally Verified Proof of the Prime Number Theorem
journal contribution
posted on 2007-01-01, 00:00 authored by Jeremy AvigadJeremy Avigad, Kevin Donnelly, David Gray, Paul RaffThe 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.