A formally verified proof of the prime number theorem

Simple item page
dc.creatorAvigad, Jeremy
dc.creatorDonnelly, Kevin
dc.creatorGray, David
dc.creatorRaff, Paul
dc.date2005-09-09
dc.date2006-04-06
dc.date.accessioned2026-07-07T06:41:57Z
dc.date.available2026-07-07T06:41:57Z
dc.descriptionThe 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.
dc.description23 pages
dc.identifierhttps://arxiv.org/abs/cs/0509025
dc.identifierhttp://arxiv.org/abs/cs/0509025
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/101859
dc.subjectArtificial Intelligence
dc.subjectLogic in Computer Science
dc.subjectSymbolic Computation
dc.subjectF.4.1; I.2.3
dc.titleA formally verified proof of the prime number theorem
dc.typetext

Files

Collections

arXiv