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