From f87b0331bce8eb76069e37535328b4e17498f783 Mon Sep 17 00:00:00 2001 From: faenuccio Date: Sat, 3 Feb 2024 19:35:57 +0100 Subject: [PATCH 1/4] added three refs --- lean.bib | 67 ++++++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 55 insertions(+), 12 deletions(-) diff --git a/lean.bib b/lean.bib index 869823e3ae..bb352ffa70 100644 --- a/lean.bib +++ b/lean.bib @@ -148,21 +148,64 @@ @InProceedings{ BaanenBCD23 bibsource = {dblp computer science bibliography, https://dblp.org} } -@Misc{ BaanenDahmenNarayananNuccio21, - title = {A formalization of {D}edekind domains and class groups of - global fields}, - author = {Anne Baanen and Sander R. Dahmen and Ashvni Narayanan and - Filippo A. E. Nuccio}, - year = {2021}, - eprint = {2102.02600}, - archiveprefix = {arXiv}, - primaryclass = {cs.LO}, - url = {https://arxiv.org/abs/2102.02600}, - website = {https://github.com/lean-forward/class-number}, +@InProceedings{BaanenDahmenNarayananNuccio21, + author = {Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni and N{uccio Mortarino Majno di Capriglio}, Filippo A. E.}, + title = {{A Formalization of Dedekind Domains and Class Groups of Global Fields}}, + booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, + pages = {5:1--5:19}, + series = {Leibniz International Proceedings in Informatics (LIPIcs)}, + ISBN = {978-3-95977-188-7}, + ISSN = {1868-8969}, + year = {2021}, + volume = {193}, + editor = {Cohen, Liron and Kaliszyk, Cezary}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, + address = {Dagstuhl, Germany}, + URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.5}, + URN = {urn:nbn:de:0030-drops-139004}, + doi = {10.4230/LIPIcs.ITP.2021.5}, + annote = {Keywords: formal math, algebraic number theory, commutative algebra, Lean, mathlib}, + tags = {formalization, lean3}, +} + +@article{BaanenDahmenNarayananNuccio22, + AUTHOR = {Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni and + N{uccio Mortarino Majno di Capriglio}, Filippo A. E.}, + TITLE = {A formalization of {D}edekind domains and class groups of global fields}, + JOURNAL = {J. Automat. Reason.}, + FJOURNAL = {Journal of Automated Reasoning}, + VOLUME = {66}, + YEAR = {2022}, + NUMBER = {4}, + PAGES = {611--637}, + ISSN = {0168-7433,1573-0670}, + MRCLASS = {03B35 (11R29 13C20)}, + MRNUMBER = {4505023}, + DOI = {10.1007/s10817-022-09644-0}, + URL = {https://doi.org/10.1007/s10817-022-09644-0}, tags = {formalization, lean3}, - note = {To be presented at ITP 2021} } +@inproceedings{deFNuc, + author = {de Frutos-Fern\'{a}ndez, Mar\'{\i}a In\'{e}s and N{uccio Mortarino Majno di Capriglio, Filippo A. E.}}, + title = {A Formalization of Complete Discrete Valuation Rings and Local Fields}, + year = {2024}, + isbn = {9798400704888}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + url = {https://doi.org/10.1145/3636501.3636942}, + doi = {10.1145/3636501.3636942}, + abstract = {Local fields, and fields complete with respect to a discrete valuation, are essential objects in commutative algebra, with applications to number theory and algebraic geometry. We formalize in Lean the basic theory of discretely valued fields. In particular, we prove that the unit ball with respect to a discrete valuation on a field is a discrete valuation ring and, conversely, that the adic valuation on the field of fractions of a discrete valuation ring is discrete. We define finite extensions of valuations and of discrete valuation rings, and prove some localization results. Building on this general theory, we formalize the abstract definition and some fundamental properties of local fields. As an application, we show that finite extensions of the field ℚp of p-adic numbers and of the field Fp((X)) of Laurent series over Fp are local fields.}, + booktitle = {Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs}, + pages = {190–204}, + numpages = {15}, + keywords = {mathlib, local fields, formal mathematics, discrete valuation rings, algebraic number theory, Lean}, + location = {, London, UK, }, + series = {CPP 2024}, + tags = {formalization, lean3}, +} + + @Booklet{ Best2021, author = {Alexander Best}, title = {Automatically Generalizing Theorems Using Typeclasses}, From 51a8be85c3819c405024fe8ea4954f70d6fe6c5d Mon Sep 17 00:00:00 2001 From: faenuccio Date: Sun, 4 Feb 2024 11:05:56 +0100 Subject: [PATCH 2/4] formatting --- lean.bib | 112 ++++++++++++++++++++++++++++--------------------------- 1 file changed, 57 insertions(+), 55 deletions(-) diff --git a/lean.bib b/lean.bib index bb352ffa70..9834b4cb53 100644 --- a/lean.bib +++ b/lean.bib @@ -148,61 +148,63 @@ @InProceedings{ BaanenBCD23 bibsource = {dblp computer science bibliography, https://dblp.org} } -@InProceedings{BaanenDahmenNarayananNuccio21, - author = {Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni and N{uccio Mortarino Majno di Capriglio}, Filippo A. E.}, - title = {{A Formalization of Dedekind Domains and Class Groups of Global Fields}}, - booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, - pages = {5:1--5:19}, - series = {Leibniz International Proceedings in Informatics (LIPIcs)}, - ISBN = {978-3-95977-188-7}, - ISSN = {1868-8969}, - year = {2021}, - volume = {193}, - editor = {Cohen, Liron and Kaliszyk, Cezary}, - publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, - address = {Dagstuhl, Germany}, - URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.5}, - URN = {urn:nbn:de:0030-drops-139004}, - doi = {10.4230/LIPIcs.ITP.2021.5}, - annote = {Keywords: formal math, algebraic number theory, commutative algebra, Lean, mathlib}, - tags = {formalization, lean3}, -} - -@article{BaanenDahmenNarayananNuccio22, - AUTHOR = {Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni and - N{uccio Mortarino Majno di Capriglio}, Filippo A. E.}, - TITLE = {A formalization of {D}edekind domains and class groups of global fields}, - JOURNAL = {J. Automat. Reason.}, - FJOURNAL = {Journal of Automated Reasoning}, - VOLUME = {66}, - YEAR = {2022}, - NUMBER = {4}, - PAGES = {611--637}, - ISSN = {0168-7433,1573-0670}, - MRCLASS = {03B35 (11R29 13C20)}, - MRNUMBER = {4505023}, - DOI = {10.1007/s10817-022-09644-0}, - URL = {https://doi.org/10.1007/s10817-022-09644-0}, - tags = {formalization, lean3}, -} - -@inproceedings{deFNuc, - author = {de Frutos-Fern\'{a}ndez, Mar\'{\i}a In\'{e}s and N{uccio Mortarino Majno di Capriglio, Filippo A. E.}}, - title = {A Formalization of Complete Discrete Valuation Rings and Local Fields}, - year = {2024}, - isbn = {9798400704888}, - publisher = {Association for Computing Machinery}, - address = {New York, NY, USA}, - url = {https://doi.org/10.1145/3636501.3636942}, - doi = {10.1145/3636501.3636942}, - abstract = {Local fields, and fields complete with respect to a discrete valuation, are essential objects in commutative algebra, with applications to number theory and algebraic geometry. We formalize in Lean the basic theory of discretely valued fields. In particular, we prove that the unit ball with respect to a discrete valuation on a field is a discrete valuation ring and, conversely, that the adic valuation on the field of fractions of a discrete valuation ring is discrete. We define finite extensions of valuations and of discrete valuation rings, and prove some localization results. Building on this general theory, we formalize the abstract definition and some fundamental properties of local fields. As an application, we show that finite extensions of the field ℚp of p-adic numbers and of the field Fp((X)) of Laurent series over Fp are local fields.}, - booktitle = {Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs}, - pages = {190–204}, - numpages = {15}, - keywords = {mathlib, local fields, formal mathematics, discrete valuation rings, algebraic number theory, Lean}, - location = {, London, UK, }, - series = {CPP 2024}, - tags = {formalization, lean3}, +@InProceedings{ BaanenDahmenNarayananNuccio21, + author = {Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni and + N{uccio Mortarino Majno di Capriglio}, Filippo A. E.}, + title = {A Formalization of {D}edekind {D}omains an + {C}lass {G}roups of {G}lobal {F}ields}, + booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, + pages = {5:1--5:19}, + series = {Leibniz International Proceedings in Informatics (LIPIcs)}, + ISBN = {978-3-95977-188-7}, + ISSN = {1868-8969}, + year = {2021}, + volume = {193}, + editor = {Cohen, Liron and Kaliszyk, Cezary}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, + address = {Dagstuhl, Germany}, + url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.5}, + urn = {urn:nbn:de:0030-drops-139004}, + doi = {10.4230/LIPIcs.ITP.2021.5}, + annote = {Keywords: formal math, algebraic number theory, commutative algebra, Lean, mathlib}, + tags = {formalization, lean3}, +} + +@article{ BaanenDahmenNarayananNuccio22, + author = {Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni and + N{uccio Mortarino Majno di Capriglio}, Filippo A. E.}, + title = {A formalization of {D}edekind domains and class groups of global fields}, + journal = {J. Automat. Reason.}, + fjournal = {Journal of Automated Reasoning}, + volume = {66}, + year = {2022}, + number = {4}, + pages = {611--637}, + issn = {0168-7433,1573-0670}, + mrclass = {03B35 (11R29 13C20)}, + mrnumber = {4505023}, + doi = {10.1007/s10817-022-09644-0}, + url = {https://doi.org/10.1007/s10817-022-09644-0}, + tags = {formalization, lean3}, +} + +@inproceedings{ deFrutosNuccio24, + author = {de Frutos-Fern\'{a}ndez, Mar\'{\i}a In\'{e}s and + N{uccio Mortarino Majno di Capriglio, Filippo A. E.}}, + title = {A {F}ormalization of {C}omplete {D}iscrete {V}aluation {R}ings and + {L}ocal {F}ields}, + year = {2024}, + isbn = {9798400704888}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + url = {https://doi.org/10.1145/3636501.3636942}, + doi = {10.1145/3636501.3636942}, + booktitle = {Proceedings of the 13th ACM SIGPLAN International Conference on + Certified Programs and Proofs}, + pages = {190–204}, + numpages = {15}, + series = {CPP 2024}, + tags = {formalization, lean3}, } From 2ee5e8e72cb0a83afd1cd127870e0b062f79f840 Mon Sep 17 00:00:00 2001 From: faenuccio Date: Sun, 4 Feb 2024 11:18:18 +0100 Subject: [PATCH 3/4] run bibtool --- lean.bib | 117 ++++++++++++++++++++++++++++--------------------------- 1 file changed, 60 insertions(+), 57 deletions(-) diff --git a/lean.bib b/lean.bib index 9834b4cb53..b8f5c68378 100644 --- a/lean.bib +++ b/lean.bib @@ -148,65 +148,49 @@ @InProceedings{ BaanenBCD23 bibsource = {dblp computer science bibliography, https://dblp.org} } -@InProceedings{ BaanenDahmenNarayananNuccio21, - author = {Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni and - N{uccio Mortarino Majno di Capriglio}, Filippo A. E.}, - title = {A Formalization of {D}edekind {D}omains an - {C}lass {G}roups of {G}lobal {F}ields}, - booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, - pages = {5:1--5:19}, - series = {Leibniz International Proceedings in Informatics (LIPIcs)}, - ISBN = {978-3-95977-188-7}, - ISSN = {1868-8969}, - year = {2021}, - volume = {193}, - editor = {Cohen, Liron and Kaliszyk, Cezary}, - publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, - address = {Dagstuhl, Germany}, - url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.5}, - urn = {urn:nbn:de:0030-drops-139004}, - doi = {10.4230/LIPIcs.ITP.2021.5}, - annote = {Keywords: formal math, algebraic number theory, commutative algebra, Lean, mathlib}, - tags = {formalization, lean3}, -} - -@article{ BaanenDahmenNarayananNuccio22, - author = {Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni and - N{uccio Mortarino Majno di Capriglio}, Filippo A. E.}, - title = {A formalization of {D}edekind domains and class groups of global fields}, - journal = {J. Automat. Reason.}, - fjournal = {Journal of Automated Reasoning}, - volume = {66}, - year = {2022}, - number = {4}, - pages = {611--637}, - issn = {0168-7433,1573-0670}, - mrclass = {03B35 (11R29 13C20)}, - mrnumber = {4505023}, - doi = {10.1007/s10817-022-09644-0}, - url = {https://doi.org/10.1007/s10817-022-09644-0}, - tags = {formalization, lean3}, -} - -@inproceedings{ deFrutosNuccio24, - author = {de Frutos-Fern\'{a}ndez, Mar\'{\i}a In\'{e}s and - N{uccio Mortarino Majno di Capriglio, Filippo A. E.}}, - title = {A {F}ormalization of {C}omplete {D}iscrete {V}aluation {R}ings and - {L}ocal {F}ields}, - year = {2024}, - isbn = {9798400704888}, - publisher = {Association for Computing Machinery}, - address = {New York, NY, USA}, - url = {https://doi.org/10.1145/3636501.3636942}, - doi = {10.1145/3636501.3636942}, - booktitle = {Proceedings of the 13th ACM SIGPLAN International Conference on - Certified Programs and Proofs}, - pages = {190–204}, - numpages = {15}, - series = {CPP 2024}, - tags = {formalization, lean3}, +@InProceedings{ BaanenDahmenNarayananNuccio21, + author = {Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni + and N{uccio Mortarino Majno di Capriglio}, Filippo A. E.}, + title = {A Formalization of {D}edekind {D}omains an {C}lass + {G}roups of {G}lobal {F}ields}, + booktitle = {12th International Conference on Interactive Theorem + Proving (ITP 2021)}, + pages = {5:1--5:19}, + series = {Leibniz International Proceedings in Informatics + (LIPIcs)}, + isbn = {978-3-95977-188-7}, + issn = {1868-8969}, + year = {2021}, + volume = {193}, + editor = {Cohen, Liron and Kaliszyk, Cezary}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, + address = {Dagstuhl, Germany}, + url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.5}, + urn = {urn:nbn:de:0030-drops-139004}, + doi = {10.4230/LIPIcs.ITP.2021.5}, + annote = {Keywords: formal math, algebraic number theory, + commutative algebra, Lean, mathlib}, + tags = {formalization, lean3} } +@Article{ BaanenDahmenNarayananNuccio22, + author = {Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni + and N{uccio Mortarino Majno di Capriglio}, Filippo A. E.}, + title = {A formalization of {D}edekind domains and class groups of + global fields}, + journal = {J. Automat. Reason.}, + fjournal = {Journal of Automated Reasoning}, + volume = {66}, + year = {2022}, + number = {4}, + pages = {611--637}, + issn = {0168-7433,1573-0670}, + mrclass = {03B35 (11R29 13C20)}, + mrnumber = {4505023}, + doi = {10.1007/s10817-022-09644-0}, + url = {https://doi.org/10.1007/s10817-022-09644-0}, + tags = {formalization, lean3} +} @Booklet{ Best2021, author = {Alexander Best}, @@ -469,6 +453,25 @@ @InProceedings{ deFrutos23 tags = {formalization, lean3} } +@InProceedings{ deFrutosNuccio24, + author = {de Frutos-Fern\'{a}ndez, Mar\'{\i}a In\'{e}s and N{uccio + Mortarino Majno di Capriglio, Filippo A. E.}}, + title = {A {F}ormalization of {C}omplete {D}iscrete {V}aluation + {R}ings and {L}ocal {F}ields}, + year = {2024}, + isbn = {9798400704888}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + url = {https://doi.org/10.1145/3636501.3636942}, + doi = {10.1145/3636501.3636942}, + booktitle = {Proceedings of the 13th ACM SIGPLAN International + Conference on Certified Programs and Proofs}, + pages = {190–204}, + numpages = {15}, + series = {CPP 2024}, + tags = {formalization, lean3} +} + @Misc{ DeMoura15, author = "{de Moura}, Leonardo and Avigad, Jeremy and Kong, Soonho and Roux, Cody", From ab2b57a671e4b197ce8cb8f5e3cb9014b9d4d143 Mon Sep 17 00:00:00 2001 From: faenuccio Date: Sun, 4 Feb 2024 11:23:45 +0100 Subject: [PATCH 4/4] added two more refs and run bibtool --- lean.bib | 56 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 56 insertions(+) diff --git a/lean.bib b/lean.bib index b8f5c68378..655d56f837 100644 --- a/lean.bib +++ b/lean.bib @@ -192,6 +192,25 @@ @Article{ BaanenDahmenNarayananNuccio22 tags = {formalization, lean3} } +@Article{ BaanenDahmenNarayananNuccio22, + author = {Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni + and N{uccio Mortarino Majno di Capriglio}, Filippo A. E.}, + title = {A formalization of {D}edekind domains and class groups of + global fields}, + journal = {J. Automat. Reason.}, + fjournal = {Journal of Automated Reasoning}, + volume = {66}, + year = {2022}, + number = {4}, + pages = {611--637}, + issn = {0168-7433,1573-0670}, + mrclass = {03B35 (11R29 13C20)}, + mrnumber = {4505023}, + doi = {10.1007/s10817-022-09644-0}, + url = {https://doi.org/10.1007/s10817-022-09644-0}, + tags = {formalization, lean3} +} + @Booklet{ Best2021, author = {Alexander Best}, title = {Automatically Generalizing Theorems Using Typeclasses}, @@ -453,6 +472,43 @@ @InProceedings{ deFrutos23 tags = {formalization, lean3} } +@InProceedings{ deFrutosNuccio24, + author = {de Frutos-Fern\'{a}ndez, Mar\'{\i}a In\'{e}s and N{uccio + Mortarino Majno di Capriglio, Filippo A. E.}}, + title = {A Formalization of Complete Discrete Valuation Rings and + Local Fields}, + year = {2024}, + isbn = {9798400704888}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + url = {https://doi.org/10.1145/3636501.3636942}, + doi = {10.1145/3636501.3636942}, + abstract = {Local fields, and fields complete with respect to a + discrete valuation, are essential objects in commutative + algebra, with applications to number theory and algebraic + geometry. We formalize in Lean the basic theory of + discretely valued fields. In particular, we prove that the + unit ball with respect to a discrete valuation on a field + is a discrete valuation ring and, conversely, that the adic + valuation on the field of fractions of a discrete valuation + ring is discrete. We define finite extensions of valuations + and of discrete valuation rings, and prove some + localization results. Building on this general theory, we + formalize the abstract definition and some fundamental + properties of local fields. As an application, we show that + finite extensions of the field ℚp of p-adic numbers and + of the field Fp((X)) of Laurent series over Fp are local + fields.}, + booktitle = {Proceedings of the 13th ACM SIGPLAN International + Conference on Certified Programs and Proofs}, + pages = {190–204}, + numpages = {15}, + keywords = {mathlib, local fields, formal mathematics, discrete + valuation rings, algebraic number theory, Lean}, + series = {CPP 2024}, + tags = {formalization, lean3} +} + @InProceedings{ deFrutosNuccio24, author = {de Frutos-Fern\'{a}ndez, Mar\'{\i}a In\'{e}s and N{uccio Mortarino Majno di Capriglio, Filippo A. E.}},