{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,23]],"date-time":"2025-03-23T04:22:52Z","timestamp":1742703772721,"version":"3.40.2"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2025,2,4]],"date-time":"2025-02-04T00:00:00Z","timestamp":1738627200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,2,4]],"date-time":"2025-02-04T00:00:00Z","timestamp":1738627200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"name":"Beijing University of Chemical Technology RC","award":["202145"],"award-info":[{"award-number":["202145"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,3]]},"DOI":"10.1007\/s10817-025-09718-9","type":"journal-article","created":{"date-parts":[[2025,2,4]],"date-time":"2025-02-04T09:58:11Z","timestamp":1738663091000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formalization of the Prime Number Theorem with a Remainder Term"],"prefix":"10.1007","volume":"69","author":[{"given":"Shuhao","family":"Song","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bowen","family":"Yao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,2,4]]},"reference":[{"issue":"1","key":"9718_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/1297658.1297660","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 (2007). https:\/\/doi.org\/10.1145\/1297658.1297660","journal-title":"ACM Trans. Comput. Log."},{"key":"9718_CR2","doi-asserted-by":"publisher","unstructured":"Bartle, R.: A Modern Theory of Integration (2001). https:\/\/doi.org\/10.1090\/gsm\/032","DOI":"10.1090\/gsm\/032"},{"key":"9718_CR3","unstructured":"Carneiro, M.M.: Formalization of the prime number theorem and Dirichlet\u2019s theorem. In: FM4M\/MathUI\/ThEdu\/DP\/WIP@CIKM, 2016 (2016). https:\/\/api.semanticscholar.org\/CorpusID:14038947"},{"key":"9718_CR4","unstructured":"Eberl, M., Paulson, L.C.: The prime number theorem. Archive of Formal Proofs (Formal proof development) (2018). https:\/\/isa-afp.org\/entries\/Prime_Number_Theorem.html"},{"key":"9718_CR5","doi-asserted-by":"publisher","unstructured":"Eberl, M.: Nine chapters of analytic number theory in Isabelle\/HOL. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), 2019, vol. 141, pp. 16-11619. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.16","DOI":"10.4230\/LIPIcs.ITP.2019.16"},{"key":"9718_CR6","doi-asserted-by":"publisher","unstructured":"Eberl, M.: Verified real asymptotics in Isabelle\/HOL. In: Proceedings of the International Symposium on Symbolic and Algebraic Computation. ISSAC \u201919, 2019. ACM, New York (2019). https:\/\/doi.org\/10.1145\/3326229.3326240","DOI":"10.1145\/3326229.3326240"},{"key":"9718_CR7","unstructured":"Eberl, M.: The Hurwitz and Riemann $$\\zeta $$ functions. Archive of Formal Proofs (Formal proof development) (2017). https:\/\/isa-afp.org\/entries\/Zeta_Function.html"},{"key":"9718_CR8","unstructured":"Freek, W.: Formalizing 100 Theorems. https:\/\/www.cs.ru.nl\/%7efreek\/100\/"},{"key":"9718_CR9","doi-asserted-by":"publisher","unstructured":"Gordon, R.A.: The Integrals of Lebesgue, Denjoy, Perron, and Henstock (1994). https:\/\/doi.org\/10.1090\/gsm\/004","DOI":"10.1090\/gsm\/004"},{"key":"9718_CR10","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/s10817-009-9145-6","volume":"43","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: Formalizing an analytic proof of the prime number theorem. J. Autom. Reason. 43, 243\u2013261 (2009). https:\/\/doi.org\/10.1007\/s10817-009-9145-6","journal-title":"J. Autom. Reason."},{"key":"9718_CR11","doi-asserted-by":"publisher","first-page":"63","DOI":"10.6092\/issn.1972-5787\/1558","volume":"2","author":"J Harrison","year":"2010","unstructured":"Harrison, J.: A formalized proof of Dirichlet\u2019s theorem on primes in arithmetic progression. J. Formaliz. Reason. 2, 63\u201383 (2010). https:\/\/doi.org\/10.6092\/issn.1972-5787\/1558","journal-title":"J. Formaliz. Reason."},{"key":"9718_CR12","doi-asserted-by":"publisher","DOI":"10.2307\/3606518","volume-title":"The Distribution of Prime Numbers","author":"AE Ingham","year":"1990","unstructured":"Ingham, A.E.: The Distribution of Prime Numbers, vol. 30. Cambridge University Press, Cambridge (1990). https:\/\/doi.org\/10.2307\/3606518"},{"key":"9718_CR13","first-page":"185","volume":"13","author":"NM Korobov","year":"1958","unstructured":"Korobov, N.M.: Estimates of trigonometric sums and their applications. Uspekhi Mat. Nauk 13, 185\u2013192 (1958)","journal-title":"Uspekhi Mat. Nauk"},{"issue":"2","key":"9718_CR14","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/s10817-019-09521-3","volume":"64","author":"W Li","year":"2020","unstructured":"Li, W., Paulson, L.C.: Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle\/HOL. J. Autom. Reason. 64(2), 331\u2013360 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09521-3","journal-title":"J. Autom. Reason."},{"key":"9718_CR15","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-319-43144-4_15","volume-title":"Interactive Theorem Proving","author":"W Li","year":"2016","unstructured":"Li, W., Paulson, L.C.: A formal proof of Cauchy\u2019s residue theorem. In: Blanchette, J.C., Merz, S. (eds.) Interactive Theorem Proving, pp. 235\u2013251. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-43144-4_15"},{"key":"9718_CR16","doi-asserted-by":"publisher","first-page":"481","DOI":"10.4310\/PAMQ.2007.V3.N2.A4","volume":"3","author":"J Liu","year":"2007","unstructured":"Liu, J., Ye, Y.: Perron\u2019s formula and the prime number theorem for automorphic L-functions. Pure Appl. Math. Q. 3, 481\u2013497 (2007). https:\/\/doi.org\/10.4310\/PAMQ.2007.V3.N2.A4","journal-title":"Pure Appl. Math. Q."},{"issue":"3","key":"9718_CR17","doi-asserted-by":"publisher","first-page":"979","DOI":"10.1216\/rmjm\/1181071619","volume":"29","author":"WC Lu","year":"1999","unstructured":"Lu, W.C.: On the elementary proof of the prime number theorem with a remainder term. Rocky Mt. J. Math. 29(3), 979\u20131053 (1999). https:\/\/doi.org\/10.1216\/rmjm\/1181071619","journal-title":"Rocky Mt. J. Math."},{"issue":"1","key":"9718_CR18","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/s40993-023-00498-y","volume":"10","author":"MJ Mossinghoff","year":"2024","unstructured":"Mossinghoff, M.J., Trudgian, T.S., Yang, A.: Explicit zero-free regions for the Riemann zeta-function. Res. Number Theory 10(1), 11 (2024). https:\/\/doi.org\/10.1007\/s40993-023-00498-y","journal-title":"Res. Number Theory"},{"key":"9718_CR19","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/j.jnt.2015.05.010","volume":"157","author":"MJ Mossinghoff","year":"2015","unstructured":"Mossinghoff, M.J., Trudgian, T.S.: Nonnegative trigonometric polynomials and a zero-free region for the Riemann zeta-function. J. Number Theory 157, 329\u2013349 (2015). https:\/\/doi.org\/10.1016\/j.jnt.2015.05.010","journal-title":"J. Number Theory"},{"key":"9718_CR20","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1090\/S0025-5718-1976-0457374-X","volume":"30","author":"L Schoenfeld","year":"1976","unstructured":"Schoenfeld, L.: Sharper bounds for the Chebyshev functions $$\\theta (x)$$ and $$\\psi (x).$$ II. Math. Comput. 30, 337\u2013360 (1976). https:\/\/doi.org\/10.1090\/S0025-5718-1976-0457374-X","journal-title":"Math. Comput."},{"key":"9718_CR21","volume-title":"Complex Analysis","author":"E Stein","year":"2003","unstructured":"Stein, E., Shakarchi, R.: Complex Analysis. Princeton University Press, Princeton (2003)"},{"key":"9718_CR22","doi-asserted-by":"publisher","DOI":"10.1090\/gsm\/163","volume-title":"Introduction to Analytic and Probabilistic Number Theory","author":"G Tenenbaum","year":"2015","unstructured":"Tenenbaum, G.: Introduction to Analytic and Probabilistic Number Theory, vol. 163. American Mathematical Society, Providence (2015). https:\/\/doi.org\/10.1090\/gsm\/163"},{"key":"9718_CR23","volume-title":"The Theory of the Riemann Zeta-function","author":"EC Titchmarsh","year":"1986","unstructured":"Titchmarsh, E.C., Heath-Brown, D.R.: The Theory of the Riemann Zeta-function. Oxford University Press, Oxford (1986)"},{"key":"9718_CR24","volume-title":"The Theory of Functions","author":"EC Titchmarsh","year":"1964","unstructured":"Titchmarsh, E.C.: The Theory of Functions. Oxford University, Oxford (1964)"},{"key":"9718_CR25","first-page":"161","volume":"22","author":"IM Vinogradov","year":"1958","unstructured":"Vinogradov, I.M.: A new estimate of the function $$\\zeta (1+it)$$. Izv. Akad. Nauk SSSR Ser. Mat. 22, 161\u2013164 (1958)","journal-title":"Izv. Akad. Nauk SSSR Ser. Mat."},{"key":"9718_CR26","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1080\/00029890.1997.11990704","journal-title":"Am. Math. Mon."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09718-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09718-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09718-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T20:54:02Z","timestamp":1742676842000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09718-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,2,4]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,3]]}},"alternative-id":["9718"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09718-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2025,2,4]]},"assertion":[{"value":"9 July 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 January 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 February 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no relevant financial or non-financial interests to disclose.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"4"}}