added two more refs and run bibtool

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.}},