A Formally Verified Proof of the Prime Number Theorem
| Abstract | 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. | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | No categories specified (fix it) | |||||||||
| Options |
|
|||||||||
| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,709 |
| External links |
|
| Through your library | Only published papers are available at libraries |
Takahito Aoto (1999). Uniqueness of Normal Proofs in Implicational Intuitionistic Logic. Journal of Logic, Language and Information 8 (2):217-242.
Jeremy Avigad (2006). Mathematical Method and Proof. Synthese 153 (1):105 - 159.
J. Todd Wilson (2001). An Intuitionistic Version of Zermelo's Proof That Every Choice Set Can Be Well-Ordered. Journal of Symbolic Logic 66 (3):1121-1126.
Alexander S. Karpenko (1989). Characterization of Prime Numbers in Łukasiewicz's Logical Matrix. Studia Logica 48 (4):465 - 478.
Konstantine Arkoudas & Selmer Bringsjord (2007). Computers, Justification, and Mathematical Knowledge. Minds and Machines 17 (2).
Carlo Cellucci (2008). Why Proof? What is a Proof? In Giovanna Corsi & Rossella Lupacchini (eds.), Deduction, Computation, Experiment. Exploring the Effectiveness of Proof, pp. 1-27. Springer.
Colin Mclarty (2010). What Does It Take to Prove Fermat's Last Theorem? Grothendieck and the Logic of Number Theory. Bulletin of Symbolic Logic 16 (3):359-377.
Monthly downloads |
Added to index2010-09-14Total downloads6 ( #145,761 of 549,753 )Recent downloads (6 months)2 ( #37,450 of 549,753 )How can I increase my downloads? |

