diff --git a/lean.bib b/lean.bib
index 5534adb93..43ea9da84 100644
--- a/lean.bib
+++ b/lean.bib
@@ -71,7 +71,8 @@ @InProceedings{   Asgeirsson24
   urn           = {urn:nbn:de:0030-drops-207347},
   doi           = {10.4230/LIPIcs.ITP.2024.6},
   annote        = {Keywords: Condensed mathematics, N\"{o}beling’s theorem,
-                  Lean, Mathlib, Interactive theorem proving}
+                  Lean, Mathlib, Interactive theorem proving},
+  tags          = {formalization, lean4}
 }
 
 @Book{            Avig14,
@@ -236,7 +237,8 @@ @InProceedings{   BasoldBruinLawson24
   urn           = {urn:nbn:de:0030-drops-207368},
   doi           = {10.4230/LIPIcs.ITP.2024.8},
   annote        = {Keywords: Lean, Directed Topology, Van Kampen Theorem,
-                  Directed Homotopy Theory, Formalised Mathematics}
+                  Directed Homotopy Theory, Formalised Mathematics},
+  tags          = {formalization, lean4}
 }
 
 @Booklet{         Best2021,
@@ -292,7 +294,8 @@ @InProceedings{   BhatKeizerHughesGoensGrosser24
   urn           = {urn:nbn:de:0030-drops-207372},
   doi           = {10.4230/LIPIcs.ITP.2024.9},
   annote        = {Keywords: compilers, semantics, mechanization, MLIR, SSA,
-                  regions, peephole rewrites}
+                  regions, peephole rewrites},
+  tags          = {formalization, lean4}
 }
 
 @Article{         BordgCavalleri2021,
@@ -443,7 +446,8 @@ @InProceedings{   CluneQianBentkampAvigad24
   urn           = {urn:nbn:de:0030-drops-207381},
   doi           = {10.4230/LIPIcs.ITP.2024.10},
   annote        = {Keywords: proof search, automatic theorem proving,
-                  interactive theorem proving, Lean, dependent type theory}
+                  interactive theorem proving, Lean, dependent type theory},
+  tags          = {formalization, lean4}
 }
 
 @InProceedings{   CommelinLewis21,
@@ -773,6 +777,30 @@ @Article{         DupuisLewisMacbeth22
   tags          = {formalization, lean3}
 }
 
+@InProceedings{   dvorak_et_al:LIPIcs.ITP.2023.15,
+  author        = {Dvorak, Martin and Blanchette, Jasmin},
+  title         = {{Closure Properties of General Grammars – Formally
+                  Verified}},
+  booktitle     = {14th International Conference on Interactive Theorem
+                  Proving (ITP 2023)},
+  pages         = {15:1--15:16},
+  series        = {Leibniz International Proceedings in Informatics
+                  (LIPIcs)},
+  isbn          = {978-3-95977-284-6},
+  issn          = {1868-8969},
+  year          = {2023},
+  volume        = {268},
+  editor        = {Naumowicz, Adam and Thiemann, Ren\'{e}},
+  publisher     = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
+  address       = {Dagstuhl, Germany},
+  url           = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.15},
+  urn           = {urn:nbn:de:0030-drops-183906},
+  doi           = {10.4230/LIPIcs.ITP.2023.15},
+  annote        = {Keywords: Lean, type-0 grammars, recursively enumerable
+                  languages, Kleene star},
+  tags          = {formalization, lean3}
+}
+
 @Article{         EURAM17,
   author        = {Gabriel Ebner and Sebastian Ullrich and Jared Roesch and
                   Jeremy Avigad and Leonardo {de Moura}},
@@ -810,7 +838,8 @@ @InProceedings{   Ezeh24
   urn           = {urn:nbn:de:0030-drops-207690},
   doi           = {10.4230/LIPIcs.ITP.2024.41},
   annote        = {Keywords: Interactive theorem proving, Lean4, Graphical
-                  User Interface}
+                  User Interface},
+  tags          = {formalization, lean4}
 }
 
 @Misc{            FernandezMir19,
@@ -1152,7 +1181,8 @@ @InProceedings{   Massot24
   urn           = {urn:nbn:de:0030-drops-207550},
   doi           = {10.4230/LIPIcs.ITP.2024.27},
   annote        = {Keywords: mathematics teaching, proof assistant,
-                  controlled natural language}
+                  controlled natural language},
+  tags          = {formalization, lean4}
 }
 
 @InProceedings{   Mathlib,
@@ -1281,7 +1311,8 @@ @InProceedings{   ObendraufBaanenKoopmanStebletsova24
   doi           = {10.4230/LIPIcs.ITP.2024.28},
   annote        = {Keywords: Multi-agent systems, Coalition Logic, Epistemic
                   Logic, common knowledge, completeness, formal methods, Lean
-                  prover}
+                  prover},
+  tags          = {formalization, lean4}
 }
 
 @Article{         PNWT22,
@@ -1520,7 +1551,8 @@ @InProceedings{   SubercaseauxNawrockiGallicchioCodelCarneiroHeule24
   urn           = {urn:nbn:de:0030-drops-207633},
   doi           = {10.4230/LIPIcs.ITP.2024.35},
   annote        = {Keywords: Empty Hexagon Number, Discrete Computational
-                  Geometry, Erd\H{o}s-Szekeres}
+                  Geometry, Erd\H{o}s-Szekeres},
+  tags          = {formalization, lean4}
 }
 
 @InProceedings{   TassarottiVBT21,
@@ -1649,7 +1681,8 @@ @InProceedings{   vanDoornMacbeth24
   urn           = {urn:nbn:de:0030-drops-207657},
   doi           = {10.4230/LIPIcs.ITP.2024.37},
   annote        = {Keywords: Sobolev inequality, measure theory, Lean,
-                  formalized mathematics}
+                  formalized mathematics},
+  tags          = {formalization, lean4}
 }
 
 @Misc{            VonRaumer15,
@@ -1783,3 +1816,26 @@ @InProceedings{   YingDegenne23
   bibsource     = {dblp computer science bibliography, https://dblp.org},
   tags          = {formalization, lean3}
 }
+
+@InProceedings{   Zhang23,
+  author        = {Zhang, Jujian},
+  title         = {{Formalising the Proj Construction in Lean}},
+  booktitle     = {14th International Conference on Interactive Theorem
+                  Proving (ITP 2023)},
+  pages         = {35:1--35:17},
+  series        = {Leibniz International Proceedings in Informatics
+                  (LIPIcs)},
+  isbn          = {978-3-95977-284-6},
+  issn          = {1868-8969},
+  year          = {2023},
+  volume        = {268},
+  editor        = {Naumowicz, Adam and Thiemann, Ren\'{e}},
+  publisher     = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
+  address       = {Dagstuhl, Germany},
+  url           = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.35},
+  urn           = {urn:nbn:de:0030-drops-184105},
+  doi           = {10.4230/LIPIcs.ITP.2023.35},
+  annote        = {Keywords: Lean, formalisation, algebraic geometry, scheme,
+                  Proj construction, projective geometry},
+  tags          = {formalization, lean3}
+}