lean.bib

@InProceedings{lean-tactics,
 author = {Ebner, G. and Ullrich, S. and Roesch, J. and Avigad, J. and de Moura, L.},
 title = {A metaprogramming framework for formal verification},
 year = {2017},
 issue_date = {August 2017},
 publisher = {ACM},
address = {New York, USA},
 doi = {10.1145/3110278},
 booktitle = {ICFP 2017},
 series = {PACMPL},
 number = {1, ICFP},
 month = aug,
 articleno = {Article 34},
 numpages = {29},
 keywords = {dependent type theory, theorem proving, metaprogramming, tactic language}
}

@inproceedings {frohlich,
 author = {Fr\"{o}hlich, A.},
 title = {Local fields},
 booktitle = {Algebraic {N}umber {T}heory ({P}roc. {I}nstructional {C}onf., {B}righton, 1965) },
 pages = {1--41},
 publisher = {Thompson},
 address = {Washington, D.C.},
 year = {1967},
}

@article{Cla66,
author = {Luther Claborn},
title = {{Every abelian group is a class group.}},
volume = {18},
journal = {Pacific Journal of Mathematics},
number = {2},
publisher = {Pacific Journal of Mathematics, A Non-profit Corporation},
pages = {219 -- 222},
year = {1966},
doi = {pjm/1102994263},
URL = {https://doi.org/}
}

@InProceedings{lean-prover,
 author = {de Moura, L. and Kong, S. and Avigad, J. and van Doorn, F. and von Raumer, J.},
 editor = {Felty, A. P. and Middeldorp, A.},
 title = {The {L}ean theorem prover (system description)},
 booktitle = {Automated Deduction - CADE-25},
 series = {LNCS},
 volume = {9195},
 year = {2015},
 publisher = {Springer},
 address = {Cham},
 pages = {378--388},
 doi = {10.1007/978-3-319-21401-6_26},
}

@Book{mathcomp,
 author = {Mahboubi, A.  and Tassi, E.},
 title = {The Mathematical Components Libraries},
 publisher = {Zenodo},
 address = {Genève, Switzerland},
 year = {2017},
 doi = {10.5281/zenodo.4457887},
}

@article{algebraic_hierarchy-coq,
 author = {Geuvers, H. and Pollack, R. and Wiedijk, F. and Zwanenburg, J.},
 title = {A Constructive Algebraic Hierarchy in Coq},
 year = {2002},
 issue_date = {October 2002},
 publisher = {Academic Press, Inc.},
 address = {USA},
 volume = {34},
 number = {4},
 issn = {0747-7171},
 doi = {10.1006/jsco.2002.0552},
 journal = {J. Symb. Comput.},
 month = oct,
 pages = {271–286},
 numpages = {16}
}

@inproceedings{mathlib,
 author = {{The mathlib Community}},
 editor={Blanchette, J. and Hrițcu, C.},
 title = {The {L}ean Mathematical Library},
 year = {2020},
 isbn = {9781450370974},
 publisher = {ACM},
 address = {New York, USA},
 doi = {10.1145/3372885.3373824},
 booktitle = {CPP 2020},
 pages = {367–381},
 numpages = {15},
 keywords = {formal library, mathlib, formal proof, Lean},
}

@book{Neukirch,
 author = {Neukirch, J.},
 title = {Algebraic number theory},
 series = {Fundamental Principles of Mathematical Sciences},
 volume = {322},
 note = {Translated from the 1992 German original and with a note by Norbert Schappacher, With a foreword by G. Harder},
 publisher = {Springer},
 address = {Cham},
 year = {1999},
 pages = {xviii+571},
 isbn = {3-540-65399-6},
 doi = {10.1007/978-3-662-03983-0},
}

@book{Dummit-and-Foote,
 author = {Dummit, D. S. and Foote, R. M.},
 title = {Abstract algebra},
 edition = {Third},
 publisher = {John Wiley \& Sons, Inc.},
 address = {Hoboken, NJ, USA},
 year = {2004},
 pages = {xii+932},
 isbn = {0-471-43334-9},
}

@article{gaussian_integers-isabelle,
 author = {Eberl, M.},
 title = {Gaussian Integers},
 journal = {Archive of Formal Proofs},
 month = apr,
 year = 2020,
 note = {\url{https://isa-afp.org/entries/Gaussian_Integers.html}, Formal proof development},
 ISSN = {2150-914x},
}


@article {deLima,
    AUTHOR = {de Lima, Thaynara Arielly and Galdino, Andr\'{e} Luiz and Avelar,
              Andr\'{e}ia Borges and Ayala-Rinc\'{o}n, Mauricio},
     TITLE = {Formalization of ring theory in {PVS}: isomorphism theorems,
              principal, prime and maximal ideals, {C}hinese remainder
              theorem},
   JOURNAL = {J. Automat. Reason.},
  FJOURNAL = {Journal of Automated Reasoning},
    VOLUME = {65},
      YEAR = {2021},
    NUMBER = {8},
     PAGES = {1231--1263},
      ISSN = {0168-7433},
   MRCLASS = {03B35 (13P99 16B70)},
  MRNUMBER = {4330425},
       DOI = {10.1007/s10817-021-09593-0},
       URL = {https://doi-org.docelec.univ-lyon1.fr/10.1007/s10817-021-09593-0},
}

@misc{gaussian_integers-metamath,
  author={Carneiro, M.},
  title={Definition \texttt{df-gz}},
  note={\url{http://us.metamath.org/mpeuni/df-gz.html}}
}

@inproceedings{gaussian_integers-mizar,
  author={Futa, Y. and Mizushima, D. and Okazaki, H.},
  booktitle={2012 International Symposium on Information Theory and its Applications},
  title={Formalization of {G}aussian integers, {G}aussian rational numbers, and their algebraic structures with {M}izar},
  year={2012},
  isbn={978-1-4673-2521-9},
  pages={591-595}}

@inproceedings{real-algebraic-numbers-coq,
  author    = {Cohen, C.},
  editor    = {Beringer, L. and Felty, A. P.},
  title     = {Construction of Real Algebraic Numbers in {C}oq},
  booktitle = {{ITP} 2012},
  series    = {Lecture Notes in Computer Science},
  volume    = {7406},
  pages     = {67--82},
  publisher = {Springer},
  address   = {Cham},
  year      = {2012},
  doi       = {10.1007/978-3-642-32347-8_6},
}

@misc{algebraic-numbers-ccorn,
	title = {Basics for algebraic numbers and a proof of {L}iouville’s theorem in {C-CoRN}},
	author = {Valentin Blot},
	year = {2009},
	institution = {Radboud Universiteit Nijmegen},
	note = {MSc internship report},
}

@Book{metamath,
	author = {Megill, N. D. and Wheeler, D. A.},
	title = {Metamath: A Computer Language for Mathematical Proofs},
	year = {2019},
	publisher = {Lulu Press},
	address = {Morrisville, NC, USA},
	note = {\url{http://us.metamath.org/downloads/metamath.pdf}},
}

@misc{mizar_mml,
  title = {The {M}izar Mathematical Library},
  note = {Version 5.57.1355 (04 June 2019)},
  url = {http://www.mizar.org/},
}

@inproceedings{algebraic-hierarchy_mizar,
  title = {On algebraic hierarchies in mathematical repository of {M}izar},
  author = {Grabowski, A. and Kornilowicz, A. and Schwarzweller, C.},
  booktitle = {Proceedings of the 2016 Federated Conference on Computer Science and Information Systems},
  editor = {Ganzha, M. and Maciaszek, L. and Paprzycki, M.},
  series = {ACSIS},
  volume = {8},
  pages = {363--371},
  year = {2016},
}

@misc{algebra_isabelle,
  title = {The {I}sabelle/{HOL} Algebra Library},
  author = {Ballarin~(editor), C. and Aransay, J. and Baillon, M. and de Vilhena, P.~E. and Hohe, S. and Kammüller, F. and Paulson, L.~C.},
  note = {\url{http://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/index.html}},
}

@article{algebraic-numbers-isabelle,
  author  = {Thiemann, R. and Yamada, A. and Joosten, S.},
  title   = {Algebraic Numbers in {I}sabelle/{HOL}},
  journal = {Archive of Formal Proofs},
  month   = dec,
  year    = 2015,
  note    = {\url{https://isa-afp.org/entries/Algebraic_Numbers.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@misc{algebraic-numbers-metamath,
  author = {Carneiro, M.},
  title = {Definition \texttt{df-aa}},
  note = {\url{http://us.metamath.org/mpeuni/df-aa.html}},
}

@article{algebraic-numbers-mizar,
	JOURNAL = {Formalized Mathematics},
	ISSN = {1426-2630},
	EISSN = {1898-9934},
	VOLUME = {24},
	NUMBER = {{\bf 4}},
	PAGES = {291--299},
	YEAR = {2016},
	DOI = {10.1515/forma-2016-0025},
	VERSION = {8.1.05 5.39.1282},
	TITLE = {{A}lgebraic Numbers},
	AUTHOR = {Watase, Y.},
}

@misc{fashionable-mathematics,
	title={Where is the fashionable mathematics?},
	author={Buzzard, K.},
	year={2020},
	note={\url{https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/}, accessed 2020-01-27.},
}

@misc{kash,
  author =  {Pohst, M. E. and others},
  title  =  {The Computer Algebra System {{KASH/KANT}}},
  howpublished ={\url{http://www.math.tu-berlin.de/~kant}}
}

@misc{Bra22,
  author =  {Brasca, R. and others},
  title  =  {The ring of integers of a cyclotomic field},
  howpublished ={\url{https://leanprover-community.github.io/blog/posts/the-ring-of-integers-of-a-cyclotomic-field/}},
  note = {Accessed 2022-06-20.},
}

@manual{PARI2,
	organization = "{The PARI~Group}",
	title        = "{PARI/GP version \texttt{2.11.2}}",
	year         = 2019,
	address      = "Univ. Bordeaux",
	url          = "http://pari.math.u-bordeaux.fr/"
}

@InProceedings{CapSetProblem,
  author =	{Dahmen, S. R. and H{\"o}lzl, J. and Lewis, R. Y.},
  title =	{{Formalizing the Solution to the Cap Set Problem}},
  booktitle =	{ITP 2019},
  pages =	{15:1--15:19},
  series =	{LIPIcs},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, J. and O'Leary, J. and Tolmach, A.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URN =		{urn:nbn:de:0030-drops-110703},
  doi =		{10.4230/LIPIcs.ITP.2019.15},
  annote =	{Keywords: formal proof, combinatorics, cap set problem, Lean}
}

@inproceedings{Eberl19,
  author = "Eberl, M.",
  editor = "Harrison, J. and O'Leary, J. and Tolmach, A.",
  title = "Nine Chapters of Analytic Number Theory in {I}sabelle/{HOL}",
  year = "2019",
  booktitle = "ITP 2019",
  pages = "16:1--16:19",
  series = "LIPIcs",
  doi = "10.4230/LIPIcs.ITP.2019.16",
  ISBN = "978-3-95977-122-1",
  ISSN = "1868-8969",
  volume = "141",
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
}

@article{Minkowskis_Theorem-AFP,
  author  = {Eberl, M.},
  title   = {Minkowski's Theorem},
  journal = {Archive of Formal Proofs},
  month   = jul,
  year    = 2017,
  note    = {\url{https://isa-afp.org/entries/Minkowskis_Theorem.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@book{Ireland-Rosen,
author = {Ireland, K. and Roosen, M.},
title = {A Classical Introduction to Modern Number Theory},
edition = {second},
publisher = {Springer},
address = {Cham},
year = {1990},
isbn = {978-0-387-97329-6},
}

@article{Artin-Whaples,
author = "Artin, E. and Whaples, G.",
fjournal = "Bulletin of the American Mathematical Society",
journal = "Bull. Amer. Math. Soc.",
month = "07",
number = "7",
pages = "469--492",
publisher = "American Mathematical Society",
title = "Axiomatic characterization of fields by the product formula for valuations",
url = "https://projecteuclid.org:443/euclid.bams/1183507128",
volume = "51",
year = "1945"
}

@article {Stasinski,
    AUTHOR = {Stasinski, Alexander},
     TITLE = {A uniform proof of the finiteness of the class group of a
              global field},
   JOURNAL = {Amer. Math. Monthly},
  FJOURNAL = {American Mathematical Monthly},
    VOLUME = {128},
      YEAR = {2021},
    NUMBER = {3},
     PAGES = {239--249},
      ISSN = {0002-9890},
       DOI = {10.1080/00029890.2021.1855036},
}

@article{linear-algebra-coq,
  author    = {Guillaume Cano and
               Cyril Cohen and
               Maxime D{\'{e}}n{\`{e}}s and
               Anders M{\"{o}}rtberg and
               Vincent Siles},
  title     = {Formalized linear algebra over Elementary Divisor Rings in {C}oq},
  journal   = {Logical Methods in Computer Science},
  volume    = {12},
  number    = {2},
  year      = {2016},
  doi       = {10.2168/LMCS-12(2:7)2016},
}

@inproceedings{norm_cast,
  author    = {Robert Y. Lewis and
               Paul{-}Nicolas Madelaine},
  editor    = {Pascal Fontaine and
               Konstantin Korovin and
               Ilias S. Kotsireas and
               Philipp R{\"{u}}mmer and
               Sophie Tourret},
  title     = {Simplifying Casts and Coercions (Extended Abstract)},
  booktitle = {Practical Aspects of Automated Reasoning},
  series    = {{CEUR} Workshop Proceedings},
  volume    = {2752},
  pages     = {53--62},
  publisher = {CEUR-WS.org},
  address   = {Aachen, Germany},
  year      = {2020},
  url       = {http://ceur-ws.org/Vol-2752/paper4.pdf},
  timestamp = {Tue, 09 Feb 2021 17:28:14 +0100},
  biburl    = {https://dblp.org/rec/conf/cade/LewisM20.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Book{theorem-proving-in-lean,
 author = {Avigad, Jeremy and {de Moura}, Leonardo and Kong, Soonho},
 title = {{Theorem Proving in Lean}},
 note = {Release 3.23.0, \url{https://leanprover.github.io/theorem_proving_in_lean/}},
 year = {2021},
 publisher = {Carnegie Mellon University},
 address = {Pittsburgh, PA, USA},
}

@inproceedings{typeclasses-haskell,
author = {Wadler, P. and Blott, S.},
title = {How to Make Ad-Hoc Polymorphism Less Ad Hoc},
year = {1989},
isbn = {0897912942},
publisher = {ACM},
doi = {10.1145/75277.75283},
pages = {60–76},
numpages = {17},
address = {Austin, TX, USA},
booktitle = {Principles of Programming Languages},
series = {POPL '89}
}

@book {Lang,
    AUTHOR = {Lang, Serge},
     TITLE = {Algebra},
    SERIES = {Graduate Texts in Mathematics},
    VOLUME = {211},
   EDITION = {third},
 PUBLISHER = {Springer},
   address = {Cham},
      YEAR = {2002},
     PAGES = {xvi+914},
      ISBN = {0-387-95385-X},
   MRCLASS = {00A05 (15-02)},
  MRNUMBER = {1878556},
       DOI = {10.1007/978-1-4613-0041-0},
       URL = {https://doi.org/10.1007/978-1-4613-0041-0},
}

@book {Zariski-Samuel,
    AUTHOR = {Zariski, Oscar and Samuel, Pierre},
     TITLE = {Commutative algebra, {V}olume {I}},
    SERIES = {The University Series in Higher Mathematics},
 PUBLISHER = {D. Van Nostrand Company, Inc.},
   address = {Princeton, NJ, USA},
      YEAR = {1958},
     PAGES = {xi+329},
}

@InProceedings{ClassGroupsITP2021,
  author =	{Baanen, T. and Dahmen, S. R. and {Ashvni N.} and Nuccio Mortarino Majno di Capriglio, F. A. E.},
  title =	{{A Formalization of Dedekind Domains and Class Groups of Global Fields}},
  booktitle =	{ITP 2021},
  pages =	{5:1--5:19},
  series =	{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/opus/volltexte/2021/13900},
  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}
}

@article{instance-parameters-mathlib,
  author    = {Baanen, T.},
  title     = {Use and abuse of instance parameters in the {L}ean mathematical library},
  journal   = {CoRR},
  volume    = {abs/2202.01629},
  year      = {2022},
  url       = {https://arxiv.org/abs/2202.01629},
  eprinttype = {arXiv},
  eprint    = {2202.01629},
  note      = {Accepted for publication at ITP 2022, Haifa, Israel.}
}

@misc{Maria-paper,
  doi = {10.48550/ARXIV.2203.16344},
  
  url = {https://arxiv.org/abs/2203.16344},
  
  author = {de Frutos-Fernández, María Inés},
  
  keywords = {Logic in Computer Science (cs.LO), Number Theory (math.NT), FOS: Computer and information sciences, FOS: Computer and information sciences, FOS: Mathematics, FOS: Mathematics},
  
  title = {Formalizing the Ring of Adèles of a Global Field},
  
  publisher = {arXiv},
  
  year = {2022},
  
  copyright = {arXiv.org perpetual, non-exclusive license}
}