A Formally Verified Proof of the Prime Number Theorem Jeremy Avigad Kevin Donnelly David Gray Paul Raff 10.1184/R1/6490715.v1 https://kilthub.cmu.edu/articles/journal_contribution/A_Formally_Verified_Proof_of_the_Prime_Number_Theorem/6490715 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. 2007-01-01 00:00:00 Prime number theorem formal verification