{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T19:07:55Z","timestamp":1774984075372,"version":"3.50.1"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2009,8,19]],"date-time":"2009-08-19T00:00:00Z","timestamp":1250640000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2009,10]]},"DOI":"10.1007\/s10817-009-9145-6","type":"journal-article","created":{"date-parts":[[2009,8,18]],"date-time":"2009-08-18T11:43:53Z","timestamp":1250595833000},"page":"243-261","source":"Crossref","is-referenced-by-count":28,"title":["Formalizing an Analytic Proof of the Prime Number Theorem"],"prefix":"10.1007","volume":"43","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,8,19]]},"reference":[{"key":"9145_CR1","doi-asserted-by":"crossref","first-page":"781","DOI":"10.4007\/annals.2004.160.781","volume":"160","author":"M Agrawal","year":"2004","unstructured":"Agrawal, M., Kayal, N., Saxena, N.: PRIMES is in P. Ann. Math. 160, 781\u2013793 (2004)","journal-title":"Ann. Math."},{"key":"9145_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/978-3-540-25984-8_27","volume-title":"Proceedings of the Second International Joint Conference on Automated Reasoning.","author":"J Avigad","year":"2004","unstructured":"Avigad, J., Donnelly, K.: Formalizing O notation in Isabelle\/HOL. In: Basin D., Rusinowitsch M. (eds.) Proceedings of the Second International Joint Conference on Automated Reasoning. Lecture Notes in Computer Science, vol. 3097, pp. 357\u2013371. Springer, Cork (2004)"},{"issue":"1:2","key":"9145_CR3","first-page":"1","volume":"9","author":"J Avigad","year":"2007","unstructured":"Avigad, J., Donnelly, K., Gray, D., Raff, P.: A formally verified proof of the prime number theorem. Acm Trans. Comput. Log. 9(1:2), 1\u201323 (2007)","journal-title":"Acm Trans. Comput. Log."},{"key":"9145_CR4","volume-title":"Complex Analysis","author":"J Bak","year":"1997","unstructured":"Bak, J. Newman, D.J.: Complex Analysis. Springer, New York (1997)"},{"key":"9145_CR5","first-page":"129","volume-title":"Proceedings of the IFIP TC10\/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience. IFIP Transactions A: Computer Science and Technology, vol. A-10","author":"R Boulton","year":"1993","unstructured":"Boulton, R., Gordon, A., Gordon, M., Harrison, J., Herbert, J., Van Tassel, J.: Experience with embedding hardware description languages in HOL. In: Stavridou, V., Melham, T.F., Boute, R.T. (eds.) Proceedings of the IFIP TC10\/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience. IFIP Transactions A: Computer Science and Technology, vol. A-10, pp. 129\u2013156. North-Holland, Nijmegen (1993)"},{"key":"9145_CR6","doi-asserted-by":"crossref","unstructured":"Conway, J. Kochen, S.: The free will theorem. Found. Phys. 36, 1441 (2006)","DOI":"10.1007\/s10701-006-9068-6"},{"key":"9145_CR7","first-page":"530","volume-title":"Proceedings of the Seventh International Joint Conference on Artificial Intelligence","author":"M Davis","year":"1981","unstructured":"Davis, M.: Obvious logical inferences. In: Hayes, P.J. (ed.) Proceedings of the Seventh International Joint Conference on Artificial Intelligence, pp. 530\u2013531. Kaufmann, Ingolstadt (1981)"},{"key":"9145_CR8","first-page":"163","volume-title":"Tools and Notions for Program Construction: An Advanced Course","author":"MJC Gordon","year":"1982","unstructured":"Gordon, M.J.C.: Representing a logic in the LCF metalanguage. In: N\u00e9el, D. (ed.) Tools and Notions for Program Construction: An Advanced Course, pp. 163\u2013185. Cambridge University Press, Cambridge (1982)"},{"key":"9145_CR9","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","author":"MJC Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"9145_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"MJC Gordon","year":"1979","unstructured":"Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. Lecture Notes in Computer Science, vol.\u00a078. Springer, Cambridge (1979)"},{"key":"9145_CR11","series-title":"IFIP Transactions A: Computer Science and Technology","first-page":"145","volume-title":"Proceedings of the IFIP TC10\/WG10.2 International Workshop on Higher Order Logic Theorem Proving and its Applications","author":"J Harrison","year":"1992","unstructured":"Harrison, J.: Constructing the real numbers in HOL. In: Claesen, L.J.M., Gordon, M.J.C. (eds.) Proceedings of the IFIP TC10\/WG10.2 International Workshop on Higher Order Logic Theorem Proving and its Applications. IFIP Transactions A: Computer Science and Technology, vol. A-20, pp. 145\u2013164. IMEC, Leuven (1992)"},{"key":"9145_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-1591-5","volume-title":"Theorem Proving with the Real Numbers","author":"J Harrison","year":"1998","unstructured":"Harrison, J.: Theorem Proving with the Real Numbers. Springer, New York (1998) (Revised version of author\u2019s PhD thesis)"},{"key":"9145_CR13","series-title":"Lecture Notes in Computer Science","first-page":"217","volume-title":"Formal Methods in Computer-Aided Design: Third International Conference FMCAD 2000. Lecture Notes in Computer Science","author":"J Harrison","year":"2000","unstructured":"Harrison, J.: Formal verification of floating point trigonometric functions. In: Hunt, W.A., Johnson, S.D. (eds.) Formal Methods in Computer-Aided Design: Third International Conference FMCAD 2000. Lecture Notes in Computer Science, vol. 1954, pp. 217\u2013233. Springer, New York (2000)"},{"key":"9145_CR14","unstructured":"Harrison, J.: Complex quantifier elimination in HOL. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001: Supplemental Proceedings, pp. 159\u2013174. Division of Informatics, University of Edinburgh. Published as Informatics Report Series EDI-INF-RR-0046. http:\/\/www.informatics.ed.ac.uk\/publications\/report\/0046.html (2001)"},{"key":"9145_CR15","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Isolating critical cases for reciprocals using integer factorization. In: Bajard, J.-C., Schulte, M. (eds.) Proceedings, 16th IEEE Symposium on Computer Arithmetic, pp. 148\u2013157. Santiago de Compostela, Spain. IEEE Computer Society, Los Alamitos (2003) ( http:\/\/www.dec.usc.es\/arith16\/papers\/paper-150.pdf )","DOI":"10.1109\/ARITH.2003.1207673"},{"key":"9145_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1007\/11541868_8","volume-title":"Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005","author":"J Harrison","year":"2005","unstructured":"Harrison, J.: A HOL theory of Euclidean space. In: Hurd, J., Melham, T. (eds.) Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005. Lecture Notes in Computer Science, vol. 3603, pp. 114\u2013129. Springer, Oxford (2005)"},{"key":"9145_CR17","unstructured":"Harrison, J.: The HOL light tutorial. http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light\/tutorial.pdf (2006)"},{"key":"9145_CR18","series-title":"Studies in Logic, Grammar and Rhetoric","first-page":"151","volume-title":"From Insight to Proof: Festschrift in Honour of Andrzej Trybulec","author":"J Harrison","year":"2007","unstructured":"Harrison, J.: Formalizing basic complex analysis. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar and Rhetoric, vol. 10(23), pp. 151\u2013165. University of Bia\u0142ystok, Bia\u0142ystok (2007)"},{"key":"9145_CR19","volume-title":"The Distribution of Prime Numbers","author":"AE Ingham","year":"1932","unstructured":"Ingham, A.E.: The Distribution of Prime Numbers. Cambridge University Press, Cambridge (1932)"},{"key":"9145_CR20","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139164986","volume-title":"The Prime Number Theorem. London Mathematical Society Student Texts, vol.\u00a053","author":"GJO Jameson","year":"2003","unstructured":"Jameson, G.J.O.: The Prime Number Theorem. London Mathematical Society Student Texts, vol.\u00a053. Cambridge University Press, Cambridge (2003)"},{"key":"9145_CR21","series-title":"Graduate Texts in Mathematics","volume-title":"Analytic Number Theory","author":"DJ Newman","year":"1998","unstructured":"Newman, D.J.: Analytic Number Theory. Graduate Texts in Mathematics, vol. 177. Springer, New York (1998)"},{"key":"9145_CR22","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1007\/BF00247436","volume":"3","author":"P Rudnicki","year":"1987","unstructured":"Rudnicki, P.: Obvious inferences. J. Autom. Reason. 3, 383\u2013393 (1987)","journal-title":"J. Autom. Reason."},{"key":"9145_CR23","doi-asserted-by":"crossref","unstructured":"Tenenbaum, G., France, M.M.: The Prime Numbers and Their Distribution. Student Mathematical Library, vol. 6. American Mathematical Society, Providence (2000) (Translation by Philip G. Spain, from French original \u201cNombres premiers\u201d, Presses Universitaires de France, 1997.)","DOI":"10.1090\/stml\/006"},{"key":"9145_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/978-3-540-74591-4_24","volume-title":"Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2007","author":"L Th\u00e9ry","year":"2007","unstructured":"Th\u00e9ry, L., Hanrot, G.: Primality proving with elliptic curves. In: Schneider, K., Brandt, J. (eds.) Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2007. Lecture Notes in Computer Science, vol. 4732, pp. 319\u2013333. Springer, Kaiserslautern (2007)"},{"key":"9145_CR25","unstructured":"Wiedijk, F.: The de Bruijn factor. http:\/\/www.cs.ru.nl\/~freek\/factor\/ (2000)"},{"key":"9145_CR26","volume-title":"Lecture Notes in Computer Science, vol. 3600","author":"F Wiedijk","year":"2006","unstructured":"Wiedijk, F.: The seventeen provers of the world. In: Lecture Notes in Computer Science, vol. 3600. Springer, New York (2006)"},{"key":"9145_CR27","doi-asserted-by":"crossref","DOI":"10.1142\/4132","volume-title":"A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning","author":"L Wos","year":"1999","unstructured":"Wos, L., Pieper, G.W.: A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning. World Scientific, Singapore (1999)"},{"key":"9145_CR28","doi-asserted-by":"crossref","first-page":"705","DOI":"10.1080\/00029890.1997.11990704","volume":"104","author":"D Zagier","year":"1997","unstructured":"Zagier, D.: Newman\u2019s short proof of the prime number theorem. Am. Math. Mon. 104, 705\u2013708 (1997)","journal-title":"Am. Math. Mon."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9145-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-009-9145-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9145-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,11]],"date-time":"2025-02-11T19:45:13Z","timestamp":1739303113000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-009-9145-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,8,19]]},"references-count":28,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,10]]}},"alternative-id":["9145"],"URL":"https:\/\/doi.org\/10.1007\/s10817-009-9145-6","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,8,19]]}}}