diff --git a/NOTICE b/NOTICE
index 923072afc6..b11476906e 100644
--- a/NOTICE
+++ b/NOTICE
@@ -142,6 +142,7 @@ Apache License, Version 2.0, and are redistributed here under the same license.
                                      https://github.com/lyfar/gkp-carry-lean
   LeanPool/Odlyzko                   https://github.com/ImperialCollegeLondon/FLT
   LeanPool/OrderPQ                   https://github.com/wupr/order-p-q
+  LeanPool/PDL                       https://github.com/m4lvin/lean4-pdl
   LeanPool/PFR                       https://github.com/teorth/pfr
   LeanPool/PebblingLean              https://github.com/pachterlab/P_2026_2
   LeanPool/PentagonalNumberTheorem   https://github.com/wwylele/PentagonalNumberTheorem
@@ -284,9 +285,6 @@ MIT permission notice that follows them.
       "Copyright (c) 2026" with no name; the repository owner of record is
       "SamuelSchlesinger".
 
-  LeanPool/SpecialNumbers            https://github.com/provables/special-numbers
-      Copyright (c) 2024 Walter Moreira, Joe Stubbs
-
   LeanPool/SteinhausThreeGap         https://github.com/dkunert/three-gap-theorem-lean
       Copyright (c) 2026 Dirk Kunert
 
@@ -324,10 +322,6 @@ Projects relicensed by their original author
 These projects were relicensed by their sole author before import.
 
   LeanPool/Clawristotle              https://github.com/Vilin97/Clawristotle
-  LeanPool/ForwardEuler              https://github.com/Vilin97/forward_euler
-      Originally distributed without a license file, then placed under the
-      Apache License, Version 2.0, by its sole author.
-
   LeanPool/GrothendieckVanishing     https://github.com/Vilin97/Clawristotle
       Originally distributed under the Creative Commons
       Attribution-NonCommercial-ShareAlike 4.0 International license, then
diff --git a/NOTICE.extra.yml b/NOTICE.extra.yml
index a9ff63f2c9..9e9f9758e3 100644
--- a/NOTICE.extra.yml
+++ b/NOTICE.extra.yml
@@ -59,11 +59,6 @@ FormalizationOfBoundedArithmetic:
     template text "Copyright (c) [year] [fullname]"; the repository owner of
     record is "ruplet".
 
-ForwardEuler:
-  relicensed: |-
-    Originally distributed without a license file, then placed under the
-    Apache License, Version 2.0, by its sole author.
-
 GrothendieckVanishing:
   relicensed: |-
     Originally distributed under the Creative Commons
@@ -131,9 +126,6 @@ Shannon1948Formalization:
     "Copyright (c) 2026" with no name; the repository owner of record is
     "SamuelSchlesinger".
 
-SpecialNumbers:
-  note: Copyright (c) 2024 Walter Moreira, Joe Stubbs
-
 SteinhausThreeGap:
   note: Copyright (c) 2026 Dirk Kunert
 
diff --git a/README.md b/README.md
index a3ff7653a7..dd29447593 100644
--- a/README.md
+++ b/README.md
@@ -17,7 +17,7 @@ Lean Pool sits between [`mathlib`](https://github.com/leanprover-community/mathl
 Semantic search is also available via the [API](https://search.octo.axiomatic-ai.com/api/search).
 
 <!-- BEGIN STATS -->
-**199** formalization projects · **2,850,381** lines of Lean · **2** open challenges
+**198** formalization projects · **2,883,004** lines of Lean · **2** open challenges
 <!-- END STATS -->
 
 <sub>(stats above are refreshed automatically by the [generated-metadata workflow](.github/workflows/notice.yml) — edit [`python/lean_pool/stats.py`](python/lean_pool/stats.py), not the numbers)</sub>