{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2021,9,2]],"date-time":"2021-09-02T10:47:52Z","timestamp":1630579672693},"reference-count":16,"publisher":"Association for Computing Machinery (ACM)","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2007,12]]},"abstract":"\n The prime number theorem, established by Hadamard and de la Vall\u00e9e Poussin independently in 1896, asserts that the density of primes in the positive integers is asymptotic to 1\/ln\n x<\/jats:italic>\n . Whereas their proofs made serious use of the methods of complex analysis, elementary proofs were provided by Selberg and Erd\u00f6s in 1948. We describe a formally verified version of Selberg's proof, obtained using the Isabelle proof assistant.\n <\/jats:p>","DOI":"10.1145\/1297658.1297660","type":"journal-article","created":{"date-parts":[[2007,12,21]],"date-time":"2007-12-21T14:52:36Z","timestamp":1198248756000},"page":"2","source":"Crossref","is-referenced-by-count":29,"title":["A formally verified proof of the prime number theorem"],"prefix":"10.1145","volume":"9","author":[{"given":"Jeremy","family":"Avigad","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA"}]},{"given":"Kevin","family":"Donnelly","sequence":"additional","affiliation":[{"name":"Boston University"}]},{"given":"David","family":"Gray","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA"}]},{"given":"Paul","family":"Raff","sequence":"additional","affiliation":[{"name":"Rutgers University"}]}],"member":"320","reference":[{"key":"e_1_2_1_1_1","volume-title":"Introduction to Analytic Number Theory","author":"Apostol T. M."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1093\/philmat\/11.3.257"},{"key":"e_1_2_1_3_1","volume-title":"Notes on a formalization of the prime number theorem. Tech. rep. CMU-PHIL-163","author":"Avigad J."},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Avigad J.\n and Donnelly K\n . \n 2004\n . Formalizing O notation in Isabelle\/HOL. In Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR) D. Basin and M. Rusinowitch Eds. vol. \n 3097 Lecture Notes in Artificial Intelligence Springer-Verlag 357--371. Avigad J. and Donnelly K. 2004. Formalizing O notation in Isabelle\/HOL. In Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR) D. Basin and M. Rusinowitch Eds. vol. 3097 Lecture Notes in Artificial Intelligence Springer-Verlag 357--371.","DOI":"10.1007\/978-3-540-25984-8_27"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Avigad J. and Friedman H. 2006. Combining decision procedures for the reals. Logic. Meth. Comput. Sci. 2 (4:4) 1--42. Avigad J. and Friedman H. 2006. Combining decision procedures for the reals. Logic. Meth. Comput. Sci. 2 (4:4) 1--42.","DOI":"10.2168\/LMCS-2(4:4)2006"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01270626"},{"key":"e_1_2_1_7_1","volume-title":"Riemann's Zeta Function","author":"Edwards H. M."},{"key":"e_1_2_1_8_1","unstructured":"Hardy G. H. and Wright E. M. 1979. An Introduction to the Theory of Numbers 5th Ed. Oxford University Press New York. Hardy G. H. and Wright E. M. 1979. An Introduction to the Theory of Numbers 5th Ed. Oxford University Press New York."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139164986"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_22"},{"key":"e_1_2_1_11_1","volume-title":"Elementary Methods in Number Theory","author":"Nathanson M. B."},{"key":"e_1_2_1_12_1","volume-title":"Lecture Notes in Computer Science","volume":"2283","author":"Nipkow T."},{"key":"e_1_2_1_13_1","volume-title":"Introduction to the Theory of Numbers. Pure and Applied Mathematics","author":"Shapiro H. N."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/646524.694718"},{"key":"e_1_2_1_15_1","volume-title":"thesis","author":"Wenzel M."},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","volume-title":"The Seventeen Provers of the World","author":"Wiedijk F.","DOI":"10.1007\/11542384"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1297658.1297660","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,2,19]],"date-time":"2021-02-19T19:17:04Z","timestamp":1613762224000},"score":1,"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,12]]},"references-count":16,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,12]]}},"alternative-id":["10.1145\/1297658.1297660"],"URL":"http:\/\/dx.doi.org\/10.1145\/1297658.1297660","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":["Computational Mathematics","Logic","General Computer Science","Theoretical Computer Science"],"published":{"date-parts":[[2007,12]]}}}