{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T04:09:04Z","timestamp":1772510944738,"version":"3.50.1"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2022,9,8]],"date-time":"2022-09-08T00:00:00Z","timestamp":1662595200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,9,8]],"date-time":"2022-09-08T00:00:00Z","timestamp":1662595200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["016.Vidi.189.037"],"award-info":[{"award-number":["016.Vidi.189.037"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["639.032.613"],"award-info":[{"award-number":["639.032.613"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/S021590\/1"],"award-info":[{"award-number":["EP\/S021590\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2022,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Dedekind domains and their class groups are notions in commutative algebra that are essential in algebraic number theory. We formalized these structures and several fundamental properties, including number-theoretic finiteness results for class groups, in the Lean prover as part of the  mathematical library. This paper describes the formalization process, noting the idioms we found useful in our development and \u2019s decentralized collaboration processes involved in this project.<\/jats:p>","DOI":"10.1007\/s10817-022-09644-0","type":"journal-article","created":{"date-parts":[[2022,9,8]],"date-time":"2022-09-08T17:03:53Z","timestamp":1662656633000},"page":"611-637","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["A Formalization of Dedekind Domains and Class Groups of Global Fields"],"prefix":"10.1007","volume":"66","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8497-3683","authenticated-orcid":false,"given":"Anne","family":"Baanen","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0014-0789","authenticated-orcid":false,"given":"Sander R.","family":"Dahmen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2777-4228","authenticated-orcid":false,"given":"Ashvni","family":"Narayanan","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5318-9869","authenticated-orcid":false,"given":"Filippo A. E.","family":"Nuccio Mortarino Majno di Capriglio","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,9,8]]},"reference":[{"issue":"7","key":"9644_CR1","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1090\/S0002-9904-1945-08383-9","volume":"51","author":"E Artin","year":"1945","unstructured":"Artin, E., Whaples, G.: Axiomatic characterization of fields by the product formula for valuations. Bull. Am. Math. Soc. 51(7), 469\u2013492 (1945)","journal-title":"Bull. Am. Math. Soc."},{"key":"9644_CR2","unstructured":"Avigad, J., de Moura, L., Kong, S.: Theorem Proving in Lean. Carnegie Mellon University, Pittsburgh, PA, USA (2021). Release 3.23.0, https:\/\/leanprover.github.io\/theorem_proving_in_lean\/"},{"key":"9644_CR3","doi-asserted-by":"publisher","unstructured":"Baanen, T., Dahmen, S.R., Ashvni N., Nuccio Mortarino Majno\u00a0di Capriglio, F.A.E.: A Formalization of Dedekind Domains and Class Groups of Global Fields. In: Cohen, L., Kaliszyk, C. (eds.) ITP 2021. LIPIcs, vol. 193, pp. 5\u20131519. Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2021.5. https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/13900","DOI":"10.4230\/LIPIcs.ITP.2021.5"},{"key":"9644_CR4","unstructured":"Baanen, T.: Use and abuse of instance parameters in the Lean mathematical library. CoRR abs\/2202.01629 (2022) arxiv:2202.01629. Accepted for publication at ITP 2022, Haifa, Israel"},{"key":"9644_CR5","unstructured":"Ballarin, C., Aransay, J., Baillon, M., de Vilhena, P.E., Hohe, S., Kamm\u00fcller, F., Paulson, L.C.: The Isabelle\/HOL Algebra Library. http:\/\/isabelle.in.tum.de\/dist\/library\/HOL\/HOL-Algebra\/index.html"},{"key":"9644_CR6","unstructured":"Blot, V.: Basics for algebraic numbers and a proof of Liouville\u2019s theorem in C-CoRN. MSc internship report (2009)"},{"key":"9644_CR7","unstructured":"Brasca, R., et al.: The ring of integers of a cyclotomic field. https:\/\/leanprover-community.github.io\/blog\/posts\/the-ring-of-integers-of-a-cyclotomic-field\/. Accessed 20 June 2022"},{"key":"9644_CR8","doi-asserted-by":"publisher","unstructured":"Cano, G., Cohen, C., D\u00e9n\u00e8s, M., M\u00f6rtberg, A., Siles, V.: Formalized linear algebra over elementary divisor rings in Coq. Logical Methods in Computer Science 12(2) (2016). https:\/\/doi.org\/10.2168\/LMCS-12(2:7)2016","DOI":"10.2168\/LMCS-12(2:7)2016"},{"key":"9644_CR9","unstructured":"Carneiro, M.: Definition df-aa. http:\/\/us.metamath.org\/mpeuni\/df-aa.html"},{"key":"9644_CR10","unstructured":"Carneiro, M.: Definition df-gz. http:\/\/us.metamath.org\/mpeuni\/df-gz.html"},{"issue":"2","key":"9644_CR11","doi-asserted-by":"publisher","first-page":"219","DOI":"10.2140\/pjm.1966.18.219","volume":"18","author":"L Claborn","year":"1966","unstructured":"Claborn, L.: Every abelian group is a class group. Pac. J. Math. 18(2), 219\u2013222 (1966)","journal-title":"Pac. J. Math."},{"key":"9644_CR12","doi-asserted-by":"publisher","unstructured":"Cohen, C.: Construction of real algebraic numbers in Coq. In: Beringer, L., Felty, A.P. (eds.) ITP 2012. Lecture Notes in Computer Science, vol. 7406, pp. 67\u201382. Springer, Cham (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_6","DOI":"10.1007\/978-3-642-32347-8_6"},{"key":"9644_CR13","doi-asserted-by":"publisher","unstructured":"de Frutos-Fern\u00e1ndez, M.I.: Formalizing the Ring of Ad\u00e8les of a Global Field. arXiv (2022). https:\/\/doi.org\/10.48550\/ARXIV.2203.16344. arxiv:2203.16344","DOI":"10.48550\/ARXIV.2203.16344"},{"issue":"8","key":"9644_CR14","doi-asserted-by":"publisher","first-page":"1231","DOI":"10.1007\/s10817-021-09593-0","volume":"65","author":"TA de Lima","year":"2021","unstructured":"de Lima, T.A., Galdino, A.L., Avelar, A.B., Ayala-Rinc\u00f3n, M.: Formalization of ring theory in PVS: isomorphism theorems, principal, prime and maximal ideals. Chinese remainder theorem. J. Automat. Reason. 65(8), 1231\u20131263 (2021). https:\/\/doi.org\/10.1007\/s10817-021-09593-0","journal-title":"J. Automat. Reason."},{"key":"9644_CR15","doi-asserted-by":"publisher","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) Automated Deduction - CADE-25. LNCS, vol. 9195, pp. 378\u2013388. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"9644_CR16","first-page":"932","volume-title":"Abstract Algebra","author":"DS Dummit","year":"2004","unstructured":"Dummit, D.S., Foote, R.M.: Abstract Algebra, 3rd edn., p. 932. Wiley, Hoboken (2004)","edition":"3"},{"key":"9644_CR17","unstructured":"Eberl, M.: Gaussian integers. Archive of Formal Proofs (2020). https:\/\/isa-afp.org\/entries\/Gaussian_Integers.html, Formal proof development"},{"key":"9644_CR18","unstructured":"Eberl, M.: Minkowski\u2019s theorem. Archive of Formal Proofs (2017). https:\/\/isa-afp.org\/entries\/Minkowskis_Theorem.html, Formal proof development"},{"key":"9644_CR19","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.) ITP 2019. LIPIcs, vol. 141, pp. 16\u201311619. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.16","DOI":"10.4230\/LIPIcs.ITP.2019.16"},{"key":"9644_CR20","unstructured":"Fr\u00f6hlich, A.: Local fields. In: Algebraic Number Theory (Proc. Instructional Conf., Brighton, 1965), pp. 1\u201341. Thompson, Washington, D.C. (1967)"},{"key":"9644_CR21","unstructured":"Futa, Y., Mizushima, D., Okazaki, H.: Formalization of Gaussian integers, Gaussian rational numbers, and their algebraic structures with Mizar. In: 2012 International Symposium on Information Theory and Its Applications, pp. 591\u2013595 (2012)"},{"key":"9644_CR22","doi-asserted-by":"crossref","unstructured":"Grabowski, A., Kornilowicz, A., Schwarzweller, C.: On algebraic hierarchies in mathematical repository of Mizar. In: Ganzha, M., Maciaszek, L., Paprzycki, M. (eds.) Proceedings of the 2016 Federated Conference on Computer Science and Information Systems. ACSIS, vol. 8, pp. 363\u2013371 (2016)","DOI":"10.15439\/2016F520"},{"key":"9644_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2103-4","volume-title":"A Classical Introduction to Modern Number Theory","author":"K Ireland","year":"1990","unstructured":"Ireland, K., Roosen, M.: A Classical Introduction to Modern Number Theory, 2nd edn. Springer, Cham (1990)","edition":"2"},{"key":"9644_CR24","doi-asserted-by":"publisher","unstructured":"Lang, S.: Algebra, 3rd edn. Graduate Texts in Mathematics, vol. 211, p. 914. Springer, Cham (2002). https:\/\/doi.org\/10.1007\/978-1-4613-0041-0","DOI":"10.1007\/978-1-4613-0041-0"},{"key":"9644_CR25","unstructured":"Lewis, R.Y., Madelaine, P.: Simplifying casts and coercions (extended abstract). In: Fontaine, P., Korovin, K., Kotsireas, I.S., R\u00fcmmer, P., Tourret, S. (eds.) Practical Aspects of Automated Reasoning. CEUR Workshop Proceedings, vol. 2752, pp. 53\u201362. CEUR-WS.org, Aachen, Germany (2020). http:\/\/ceur-ws.org\/Vol-2752\/paper4.pdf"},{"key":"9644_CR26","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4457887","volume-title":"The Mathematical Components Libraries","author":"A Mahboubi","year":"2017","unstructured":"Mahboubi, A., Tassi, E.: The Mathematical Components Libraries. Zenodo, Gen\u00e8ve (2017). https:\/\/doi.org\/10.5281\/zenodo.4457887"},{"key":"9644_CR27","unstructured":"Megill, N.D., Wheeler, D.A.: Metamath: A Computer Language for Mathematical Proofs. Lulu Press, Morrisville, NC, USA (2019). http:\/\/us.metamath.org\/downloads\/metamath.pdf"},{"key":"9644_CR28","doi-asserted-by":"publisher","unstructured":"Neukirch, J.: Algebraic Number Theory. Fundamental Principles of Mathematical Sciences, vol. 322, p. 571. Springer, Cham: Translated from the 1992 German original and with a note by Norbert Schappacher. With a foreword by G. Harder (1999). https:\/\/doi.org\/10.1007\/978-3-662-03983-0","DOI":"10.1007\/978-3-662-03983-0"},{"key":"9644_CR29","unstructured":"Pohst, M.E., et al.: The Computer Algebra System KASH\/KANT. http:\/\/www.math.tu-berlin.de\/~kant"},{"issue":"3","key":"9644_CR30","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1080\/00029890.2021.1855036","volume":"128","author":"A Stasinski","year":"2021","unstructured":"Stasinski, A.: A uniform proof of the finiteness of the class group of a global field. Am. Math. Monthly 128(3), 239\u2013249 (2021). https:\/\/doi.org\/10.1080\/00029890.2021.1855036","journal-title":"Am. Math. Monthly"},{"key":"9644_CR31","doi-asserted-by":"publisher","unstructured":"The mathlib Community: the Lean mathematical library. In: Blanchette, J., Hri\u0163cu, C. (eds.) CPP 2020, pp. 367\u2013381. ACM, New York, USA (2020). https:\/\/doi.org\/10.1145\/3372885.3373824","DOI":"10.1145\/3372885.3373824"},{"key":"9644_CR32","unstructured":"The PARI\u00a0Group: PARI\/GP Version 2.11.2. Univ. Bordeaux (2019). The PARI\u00a0Group. http:\/\/pari.math.u-bordeaux.fr\/"},{"key":"9644_CR33","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Yamada, A., Joosten, S.: Algebraic numbers in Isabelle\/HOL. Archive of Formal Proofs (2015). https:\/\/isa-afp.org\/entries\/Algebraic_Numbers.html, Formal proof development","DOI":"10.1007\/978-3-319-43144-4_24"},{"key":"9644_CR34","doi-asserted-by":"publisher","unstructured":"Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Principles of Programming Languages. POPL \u201989, pp. 60\u201376. ACM, Austin, TX, USA (1989). https:\/\/doi.org\/10.1145\/75277.75283","DOI":"10.1145\/75277.75283"},{"issue":"4","key":"9644_CR35","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1515\/forma-2016-0025","volume":"24","author":"Y Watase","year":"2016","unstructured":"Watase, Y.: Algebraic numbers. Formaliz. Math. 24(4), 291\u2013299 (2016). https:\/\/doi.org\/10.1515\/forma-2016-0025","journal-title":"Formaliz. Math."},{"key":"9644_CR36","unstructured":"Zariski, O., Samuel, P.: Commutative Algebra, Volume I. The University Series in Higher Mathematics, p. 329. D. Van Nostrand Company, Inc., Princeton, NJ, USA (1958)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09644-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-022-09644-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09644-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,5]],"date-time":"2022-11-05T11:20:03Z","timestamp":1667647203000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-022-09644-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,8]]},"references-count":36,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,11]]}},"alternative-id":["9644"],"URL":"https:\/\/doi.org\/10.1007\/s10817-022-09644-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,9,8]]},"assertion":[{"value":"10 September 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 August 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 September 2022","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 conflict of interest to declare that are relevant to the content of this article.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}