{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T10:48:03Z","timestamp":1776509283931,"version":"3.51.2"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032070203","type":"print"},{"value":"9783032070210","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-07021-0_23","type":"book-chapter","created":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T13:42:06Z","timestamp":1759844526000},"page":"412-430","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A PVS Library on the Infinitude of Primes"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-1943-7130","authenticated-orcid":false,"given":"Bruno Berto","family":"de Oliveira Ribeiro","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6468-9498","authenticated-orcid":false,"given":"Mariano M.","family":"Moscato","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0852-9086","authenticated-orcid":false,"given":"Thaynara Arielly","family":"de Lima","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0089-3905","authenticated-orcid":false,"given":"Mauricio","family":"Ayala-Rinc\u00f3n","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"23_CR1","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-662-57265-8","volume":"1","author":"M Aigner","year":"1999","unstructured":"Aigner, M., Ziegler, G.M.: Proofs from THE BOOK. Berlin. Germany 1(2), 12 (1999). https:\/\/doi.org\/10.1007\/978-3-662-57265-8","journal-title":"Proofs from THE BOOK. Berlin. Germany"},{"key":"23_CR2","doi-asserted-by":"publisher","unstructured":"Almeida, A.A., Oliveira, A.C.R., Ramos, T.M.F., de\u00a0Moura, F.L.C., Ayala-Rinc\u00f3n, M.: The Computational Relevance of Formal Logic Through Formal Proofs. In: Dongol, B., Petre, L., Smith, G. (eds.) Formal Methods Teaching - Third International Workshop and Tutorial, FMTea 2019, Held as Part of the Third World Congress on Formal Methods, FM 2019, Porto, Portugal, October 7, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11758, pp. 81\u201396. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-32441-4_6","DOI":"10.1007\/978-3-030-32441-4_6"},{"key":"23_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-5579-4","author":"TM Apostol","year":"2013","unstructured":"Apostol, T.M.: Introduction to analytic number theory. Springer Science & Business Media (2013). https:\/\/doi.org\/10.1007\/978-1-4757-5579-4","journal-title":"Springer Science & Business Media"},{"key":"23_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1412-0","author":"B Artmann","year":"2012","unstructured":"Artmann, B.: Euclid\u2014the creation of mathematics. Springer Science & Business Media (2012). https:\/\/doi.org\/10.1007\/978-1-4612-1412-0","journal-title":"Springer Science & Business Media"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"Ayala-Rinc\u00f3n, M., De\u00a0Moura, F.L.: Applied logic for computer scientists: computational deduction and formal proofs. Springer (2017)","DOI":"10.1007\/978-3-319-51653-0"},{"key":"23_CR6","doi-asserted-by":"publisher","unstructured":"Ayala-Rinc\u00f3n, M., de\u00a0Lima, T.A.: Teaching Interactive Proofs to Mathematicians. In: Quaresma, P., Neuper, W., Marcos, J. (eds.) Proceedings 9th International Workshop on Theorem Proving Components for Educational Software, ThEdu@IJCAR 2020, Paris, France, 29th June 2020. EPTCS, vol.\u00a0328, pp. 1\u201317 (2020). https:\/\/doi.org\/10.4204\/EPTCS.328.1","DOI":"10.4204\/EPTCS.328.1"},{"key":"23_CR7","doi-asserted-by":"publisher","unstructured":"Ayala-Rinc\u00f3n, M., de\u00a0Lima, T.A., Avelar, A.B., Galdino, A.L.: Formalization of Algebraic Theorems in PVS (Invited Talk). In: Piskac, R., Voronkov, A. (eds.) LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023. EPiC Series in Computing, vol.\u00a094, pp. 1\u201310. EasyChair (2023). https:\/\/doi.org\/10.29007\/7JBV","DOI":"10.29007\/7JBV"},{"key":"23_CR8","unstructured":"Bortin, M.: From THE BOOK: Two Squares via Involutions. Archive of Formal Proofs (August 2022), https:\/\/isa-afp.org\/entries\/Involutions2Squares.html"},{"issue":"1","key":"23_CR9","doi-asserted-by":"publisher","first-page":"28","DOI":"10.4171\/EM\/425","volume":"76","author":"D Castro","year":"2021","unstructured":"Castro, D.: Infinitude of primes: Euclid\u2019s proof using angles between lattice vectors. Elem. Math. 76(1), 28\u201332 (2021). https:\/\/doi.org\/10.4171\/EM\/425","journal-title":"Elem. Math."},{"key":"23_CR10","unstructured":"Cauchy, A.L.: Cours d\u2019analyse de L\u2019Ecole Polytechnique. oeuvres completes 2, t\u20133 (1821)"},{"key":"23_CR11","unstructured":"Eberl, M.: The Hurwitz and Riemann $$\\zeta $$ Functions. Arch. Formal Proofs (2017), https:\/\/www.isa-afp.org\/entries\/Zeta_Function.html"},{"key":"23_CR12","unstructured":"Eberl, M.: Furstenberg\u2019s topology and his proof of the infinitude of primes. Archive of Formal Proofs (2020), https:\/\/isa-afp.org\/entries\/Furstenberg_Topology.html"},{"key":"23_CR13","first-page":"1","volume":"7","author":"P Erd\u00f6s","year":"1938","unstructured":"Erd\u00f6s, P.: Uber die Reihe $$\\Sigma \\, 1\/p$$. Mathematica, Zutphen B 7, 1\u20132 (1938)","journal-title":"Mathematica, Zutphen B"},{"key":"23_CR14","unstructured":"Euler), L.E.L.: Introductio in analysin infinitorum, vol. tomus primus. Marcum-Michaelem Bousquet & Socies, Lausanne (1748)"},{"key":"23_CR15","doi-asserted-by":"publisher","unstructured":"Furstenberg, H.: On the infinitude of primes. Amer. Math. Monthly 62(5), 353 (1955). https:\/\/doi.org\/10.1080\/00029890.1955.11988641, note in Mathematical Notes, pages 349-353","DOI":"10.1080\/00029890.1955.11988641"},{"key":"23_CR16","doi-asserted-by":"publisher","unstructured":"Gauss, C.F.: Disquisitiones arithmeticae. Springer-Verlag, English edn. (1986). https:\/\/doi.org\/10.1007\/978-1-4939-7560-0","DOI":"10.1007\/978-1-4939-7560-0"},{"issue":"1","key":"23_CR17","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF01700692","volume":"38","author":"K G\u00f6del","year":"1931","unstructured":"G\u00f6del, K.: \u00dcber Formal Unentscheidbare S\u00e4tze der Principia Mathematica Und Verwandter Systeme I. Monatshefte f\u00fcr Mathematik 38(1), 173\u2013198 (1931)","journal-title":"Monatshefte f\u00fcr Mathematik"},{"issue":"6","key":"23_CR18","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1007\/S00165-012-0232-9","volume":"25","author":"H Gottliebsen","year":"2013","unstructured":"Gottliebsen, H., Hardy, R., Lightfoot, O., Martin, U.: Applications of real number theorem proving in PVS. Formal Aspects Comput. 25(6), 993\u20131016 (2013). https:\/\/doi.org\/10.1007\/S00165-012-0232-9","journal-title":"Formal Aspects Comput."},{"key":"23_CR19","unstructured":"Hua, L.K.: Introduction to number theory. Springer Science & Business Media (2012)"},{"key":"23_CR20","unstructured":"Koepke, P., Marcol, M., Sch\u00e4fer, P.: Formalizing Sets and Numbers, and some of Wiedijk\u2019s \u201c100 Theorems\u201d in Naproche (2023), https:\/\/naproche.github.io\/100_theorems.ftl.pdf, naproche repository document"},{"key":"23_CR21","unstructured":"de\u00a0Lagrange, J.L.: R\u00e9flexions sur la r\u00e9solution alg\u00e9brique des \u00e9quations. Prussian Academy (1770)"},{"key":"23_CR22","doi-asserted-by":"publisher","unstructured":"Lester, D.R.: Topology in PVS: continuous mathematics with applications. In: Proceedings of the second workshop on Automated formal methods AFM. pp. 11\u201320. ACM (2007). https:\/\/doi.org\/10.1145\/1345169.1345171","DOI":"10.1145\/1345169.1345171"},{"key":"23_CR23","unstructured":"Mendelson, B.: Introduction to topology. Dover Publications, third edn. (1990)"},{"key":"23_CR24","unstructured":"de\u00a0Oliveira\u00a0Ribeiro, B.B.: PVS formalization of proofs of the infinitude of primes (2025), Bachelor\u2019s thesis, Universidade de Bras\u00edlia. https:\/\/bdm.unb.br\/handle\/10483\/41607"},{"key":"23_CR25","doi-asserted-by":"publisher","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Proceedings 11th International Conference on Automated Deduction CADE-11. Lecture Notes in Computer Science, vol. 607, pp. 748\u2013752. Springer (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_217","DOI":"10.1007\/3-540-55602-8_217"},{"key":"23_CR26","unstructured":"Paulson, L.C.: Irrational numbers from THE BOOK. Archive of Formal Proofs (2022), https:\/\/isa-afp.org\/entries\/Irrationals_From_THEBOOK.html"},{"key":"23_CR27","doi-asserted-by":"crossref","unstructured":"Robinson, R.M.: Mersenne and Fermat numbers. Proceedings of the American Mathematical Society 5(5), 842\u2013846 (1954)","DOI":"10.1090\/S0002-9939-1954-0064787-4"},{"key":"23_CR28","volume-title":"The theory of the Riemann Zeta-function","author":"EC Titchmarsh","year":"1986","unstructured":"Titchmarsh, E.C.: The theory of the Riemann Zeta-function. The Clarendon Press, Oxford University Press (1986)"},{"key":"23_CR29","unstructured":"Vito, B.L.D.: Manip User\u2019s Guide. NASA Langley Research Center (2012), https:\/\/pvs.csl.sri.com\/doc\/manip-guide.pdf"},{"key":"23_CR30","unstructured":"Wiedijk, F.: Formalizing 100 Theorems (Formal proof\u2013getting started) (Web page, last visited February 2023), https:\/\/www.cs.ru.nl\/~freek\/100\/"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-07021-0_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T10:21:04Z","timestamp":1776507664000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-07021-0_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032070203","9783032070210"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-07021-0_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brasilia","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2025\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}