diff --git a/devops/virt/helium-os.txt b/devops/virt/helium-os.txt
index 2681f66bc..80085b2f0 100644
--- a/devops/virt/helium-os.txt
+++ b/devops/virt/helium-os.txt
@@ -1,6 +1,8 @@
 https://www.heliumos.org/
 https://codeberg.org/HeliumOS
 
+2025
+https://www.reddit.com/r/linux/comments/1m54ci4/an_exciting_new_immutable_distro_called_heliumos/
 2024
 Gosh-Its-Arch - HeliumOS: The Linux Distro that Stays Put 0:00 of 10:22
     https://www.youtube.com/watch?v=n7yILqglGo4
diff --git a/science/type-theory/hott/lean.txt b/science/type-theory/hott/lean.txt
index 23cc9984b..26ad74216 100644
--- a/science/type-theory/hott/lean.txt
+++ b/science/type-theory/hott/lean.txt
@@ -18,6 +18,11 @@ https://github.com/nomeata/loogle
 https://leanprover-community.github.io/mathlib4_docs/
 https://github.com/leanprover-community/mathlib4
 
+2025
+Petersen - FP in Lean4 with DTs
+    https://pretalx.devconf.info/devconf-cz-2025/talk/NKDGRR/
+    https://github.com/juhp/lean4-devconf.cz-2025-ws
+    https://docs.google.com/presentation/d/e/2PACX-1vT2-LH0pinThhIbth2jmTwnwSg9HY5BLmGfRTdb16jAnAiLAulOoMcL4vYe0bRQjXpVhx21gQUQyOkj/pub#slide=id.g367cee7648e_0_3
 2021
 Artem Vasilyev - Lean
     https://www.youtube.com/playlist?list=PLlVmvffm-nlI8F9uiZ62pFyzjLvOkkYLU