A formally verified proof of the prime number theorem
Artificial Intelligence
2007-05-23 v3 Logic in Computer Science
Symbolic Computation
Abstract
The prime number theorem, established by Hadamard and de la Vall'ee 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"os in 1948. We describe a formally verified version of Selberg's proof, obtained using the Isabelle proof assistant.
Keywords
Cite
@article{arxiv.cs/0509025,
title = {A formally verified proof of the prime number theorem},
author = {Jeremy Avigad and Kevin Donnelly and David Gray and Paul Raff},
journal= {arXiv preprint arXiv:cs/0509025},
year = {2007}
}
Comments
23 pages