Abstract
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 mathlib mathematical library. This paper describes the formalization process, noting the idioms we found useful in our development and mathlib's decentralized collaboration processes involved in this project.
| Original language | English |
|---|---|
| Title of host publication | 12th International Conference on Interactive Theorem Proving (ITP 2021) |
| Editors | Liron Cohen, Cezary Kaliszyk |
| Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
| Pages | 1-19 |
| Number of pages | 19 |
| ISBN (Electronic) | 9783959771887 |
| DOIs | |
| Publication status | Published - 2021 |
| Event | 12th International Conference on Interactive Theorem Proving, ITP 2021 - Virtual, Rome, Italy Duration: 29 Jun 2021 → 1 Jul 2021 |
Publication series
| Name | Leibniz International Proceedings in Informatics, LIPIcs |
|---|---|
| Volume | 193 |
| ISSN (Print) | 1868-8969 |
Conference
| Conference | 12th International Conference on Interactive Theorem Proving, ITP 2021 |
|---|---|
| Country/Territory | Italy |
| City | Virtual, Rome |
| Period | 29/06/21 → 1/07/21 |
Bibliographical note
Funding Information:Funding Anne Baanen: NWO Vidi grant No. 016.Vidi.189.037, Lean Forward Sander R. Dahmen: NWO Vidi grant No. 639.032.613, New Diophantine Directions Ashvni Narayanan: EPSRC Grant EP/S021590/1 (UK) Acknowledgements We would like to thank Jasmin Blanchette and the anonymous reviewers for useful comments on previous versions of the manuscript, which found their way into this paper. A. N. would like to thank Prof. Kevin Buzzard for his constant support and encouragement, and for introducing her to the other co-authors. A. N. and F. N. wish to express their deepest gratitude to Anne Baanen for the generosity shown along all stages of the project. Without Anne’s never-ending patience, it would have been impossible for them to contribute to this project, and to overcome several difficulties. Finally, we would like to thank the whole mathlib community for invaluable advice all along the project.
Publisher Copyright:
© Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, and Filippo A. E. Nuccio Mortarino Majno di Capriglio.
Funding
Funding Anne Baanen: NWO Vidi grant No. 016.Vidi.189.037, Lean Forward Sander R. Dahmen: NWO Vidi grant No. 639.032.613, New Diophantine Directions Ashvni Narayanan: EPSRC Grant EP/S021590/1 (UK) Acknowledgements We would like to thank Jasmin Blanchette and the anonymous reviewers for useful comments on previous versions of the manuscript, which found their way into this paper. A. N. would like to thank Prof. Kevin Buzzard for his constant support and encouragement, and for introducing her to the other co-authors. A. N. and F. N. wish to express their deepest gratitude to Anne Baanen for the generosity shown along all stages of the project. Without Anne’s never-ending patience, it would have been impossible for them to contribute to this project, and to overcome several difficulties. Finally, we would like to thank the whole mathlib community for invaluable advice all along the project.
| Funders | Funder number |
|---|---|
| Engineering and Physical Sciences Research Council | EP/S021590/1 |
| Engineering and Physical Sciences Research Council | |
| Nederlandse Organisatie voor Wetenschappelijk Onderzoek | 016, 639.032.613 |
| Nederlandse Organisatie voor Wetenschappelijk Onderzoek |
Keywords
- Algebraic number theory
- Commutative algebra
- Formal math
- Lean
- Mathlib
