add new AFM papers to paper list (#670)

Author: robertylewis

lean.bib

@@ -65,8 +65,6 @@ @InProceedings{   AngdinataXu23
   tags          = {formalization, lean3}
 }
 
-# To normalize:
-# bibtool --preserve.key.case=on --preserve.keys=on --pass.comments=on --print.use.tab=off -s -i lean.bib -o lean.bib
 @InProceedings{   Asgeirsson24,
   author        = {Asgeirsson, Dagur},
   title         = {{Towards Solid Abelian Groups: A Formal Proof of
@@ -257,6 +255,28 @@ @InProceedings{   BasoldBruinLawson24
   tags          = {formalization, lean4}
 }
 
+@Article{         BBRBvY25,
+  title         = {A complete formalization of Fermat's Last Theorem for
+                  regular primes in Lean},
+  author        = {Riccardo Brasca and Christopher Birkbeck and Eric
+                  Rodriguez Boidi and Alex Best and Ruben van De Velde and
+                  Andrew Yang},
+  url           = {https://afm.episciences.org/14586},
+  doi           = {10.46298/afm.14586},
+  journal       = {Annals of Formalized Mathematics},
+  volume        = {Volume 1},
+  eid           = 4,
+  year          = {2025},
+  month         = {Jul},
+  keywords      = {Lean, Mathlib, Kummer's lemma, [MATH.MATH-NT]Mathematics
+                  [math]/Number Theory [math.NT], [INFO.INFO-LO]Computer
+                  Science [cs]/Logic in Computer Science [cs.LO],
+                  [INFO.INFO-FL]Computer Science [cs]/Formal Languages and
+                  Automata Theory [cs.FL]},
+  language      = {English},
+  tags          = {formalization, lean4}
+}
+
 @Booklet{         Best2021,
   author        = {Alexander Best},
   title         = {Automatically Generalizing Theorems Using Typeclasses},
@@ -1169,6 +1189,21 @@ @InProceedings{   Livingston23
   tags          = {formalization, lean3}
 }
 
+@Article{         LS25,
+  title         = {Formalizing zeta and {L}-functions in Lean},
+  author        = {David Loeffler and Michael Stoll},
+  url           = {https://afm.episciences.org/15328},
+  doi           = {10.46298/afm.15328},
+  journal       = {Annals of Formalized Mathematics},
+  volume        = {Volume 1},
+  eid           = 2,
+  year          = {2025},
+  month         = {Jul},
+  keywords      = {Number Theory, Formal Languages and Automata Theory, Logic
+                  in Computer Science},
+  tags          = {formalization, lean4}
+}
+
 @Article{         Madelaine19,
   author        = {Paul{-}Nicolas Madelaine},
   title         = {Arithmetic and Casting in Lean},
@@ -1257,6 +1292,20 @@ @InProceedings{   Mehta23
   bibsource     = {dblp computer science bibliography, https://dblp.org}
 }
 
+@Article{         Merc25,
+  title         = {Formalising the local compactness of the adele ring},
+  author        = {Salvatore Mercuri},
+  url           = {https://afm.episciences.org/14840},
+  doi           = {10.46298/afm.14840},
+  journal       = {Annals of Formalized Mathematics},
+  volume        = {Volume 1},
+  eid           = 5,
+  year          = {2025},
+  month         = {Jul},
+  keywords      = {Logic in Computer Science, Number Theory},
+  tags          = {formalization, lean4}
+}
+
 @InProceedings{   Nash23,
   author        = {Nash, Oliver},
   title         = {{A Formalisation of Gallagher’s Ergodic Theorem}},
@@ -1441,6 +1490,25 @@ @Article{         PorncharoenwasePombrioTorlak2023
   tags          = {formalization, lean4}
 }
 
+@Article{         Riou25,
+  title         = {Formalization of derived categories in {L}ean/mathlib},
+  author        = {Joël Riou},
+  url           = {https://afm.episciences.org/13609},
+  doi           = {10.46298/afm.13609},
+  journal       = {Annals of Formalized Mathematics},
+  volume        = {Volume 1},
+  eid           = 1,
+  year          = {2025},
+  month         = {Jul},
+  keywords      = {Derived category, Homological algebra, Spectral sequence,
+                  MSC 2020: 18G80, 18G15, 18G40, 18E35, 68V20,
+                  [MATH.MATH-CT]Mathematics [math]/Category Theory [math.CT],
+                  [INFO.INFO-LO]Computer Science [cs]/Logic in Computer
+                  Science [cs.LO]},
+  language      = {English},
+  tags          = {formalization, lean4}
+}
+
 @Article{         SelsamDeMoura16,
   author        = {Daniel Selsam and Leonardo {de Moura}},
   title         = {Congruence Closure in Intensional Type Theory},