From e7d73c918c7f675a7d017846544f25491a3242b1 Mon Sep 17 00:00:00 2001
From: adomani <adomani@gmail.com>
Date: Thu, 4 Dec 2025 04:58:49 +0000
Subject: [PATCH 01/10] first commit

---
 Advents.lean                |   1 +
 Advents/AoC2025/day04.input | 139 ++++++++++++++++++++++++++++++++++++
 Advents/AoC2025/day04.lean  |  49 +++++++++++++
 3 files changed, 189 insertions(+)
 create mode 100644 Advents/AoC2025/day04.input
 create mode 100644 Advents/AoC2025/day04.lean

diff --git a/Advents.lean b/Advents.lean
index 0cd2edc4..c8f43034 100644
--- a/Advents.lean
+++ b/Advents.lean
@@ -2,3 +2,4 @@ import Advents.Utils
 import Advents.AoC2025.day01
 import Advents.AoC2025.day02
 import Advents.AoC2025.day03
+import Advents.AoC2025.day04
diff --git a/Advents/AoC2025/day04.input b/Advents/AoC2025/day04.input
new file mode 100644
index 00000000..983368d7
--- /dev/null
+++ b/Advents/AoC2025/day04.input
@@ -0,0 +1,139 @@
+@@@..@@@.@.@.@@@..@@@@@@@@@@@@@..@.....@@.@.@@@.@@@..@@@@@@@@..@..@@@@.@.@@@@@@....@@.@@.@@@@@@@@.@@@@@@@@@@@.@.@@.@@@@@@.@.@.@@...@@@@@@..
+@.@@.@.....@.@@@@@.@..@.@.@@@.@.@.@..@..@@@.@@..@@@.@@....@@@@.@@@..@@..@@@@.@@@@@.@@@@.@..@@@@..@@...@@@@@.@@@@@.@...@@..@@@@@..@@@@@.@@..
+@@@@..@@.....@@@@.@.@@@.@.@.@@@@@@@.@@.@@@@@.@@.@..@..@@..@@...@@@@..@@@@...@@@@.@..@.@@@.@.@@.@.@@.@@.@@@..@.@@.@@@..@.@@.@@@.@@..@@..@@@.
+@.....@.@@@@@...@@@.@@@@@@@..@.@@.@.@@@@@@@@..@.@.@@@@@@.@.@@.@.@@@@@@.@..@@@.@@@..@@@..@@@@@.@.@@.@@@@.@..@.@@@..@@...@@@.@@@@@.@..@@.@.@@
+@@@@.@@@@@@.@...@..@@..@@..@@.@@@@@...@@.@.@@@.@@...@@.@.@@@@..@.@@@.@.@@@@@@.@@@@@@@.@@..@@.@.@.@.@@...@@..@@@@@@@.@@..@@@@.@@@@@@.@@@@@..
+@@@..@@@.@@@..@@.@@.@@@@@@.@@..@...@@.@.@@@@@@@@@@@.@@@...@@..@@.@.@.@@.@@.@@..@@@@@@@@@.@@@.@@@..@@@@@..@@@@..@@.@@@@..@.@.@@.@@@@..@@@@@@
+.@@.@.@@@.@@..@@@@@.@@.@@@@..@.@@.@@@.@@...@.@..@.@@.@.@..@@.@@@.@@.@@.@@@@.@@@@@@@@...@.@.@@@@..@.@.@...@@@...@..@....@@.@@@.@@@@.@@.@@@.@
+.@..@..@@@.@@.@@......@@@@@.@@@@@.@@@@.@.@@.@@@@@@..@.@.@..@.@@@@@@....@...@.@.@@.@@.@@@@@@.@@@@@.@@@@@@......@.@@@.@.@..@@@@@@@.@.......@@
+@@.@@...@@..@@@.@.@.@...@..@.@@@@@@.@.@..@.@@.@.@@@..@@@@@@@@@...@.@@@@@...@@@@@@@@@..@@@@..@@@..@.@@@@.@@@@@@...@@.@@...@@@@..@..@@@@.@@@@
+@@@@....@.@..@@@@.@@..@@@@@@@.@@...@.@@@..@@.@@@..@.@.@@.@@@@...@@@@..@@@.@@@..@@@@@@@.@@@@@@..@@@.@.@.@@@@.@..@.@@@@@...@@.@@@@@@.@.@@@.@@
+.@@@@@@@..@.@@@@@.@.@@@@@@@@.@@.@@@@.@@@.@@@@.@@@@@.@@@.@@@@@@@..@@@@...@@@.@@.@@@..@@@@@@@.@.@...@.@@.@@.@.@@@@.@.@.@.@@@@@.@@@.@.....@@@@
+@.@..@@@...@.@@@.@..@@..@@@@.@@.@@..@@@@@@@@@@@..@@.@@...@.@@@@@@@@@.@@@.@@@@@@@@@.@.@.@@@@@.@@@..@.@@@@@.@@@.@@@@@@@........@..@.@@..@@@@@
+@@@...@.@.@...@@.@.@@.@..@@@@.@.@..@@.@@@.@..@..@@...@@.@...@.@@@@.@@.@@@.@.@@@@.@.@@@@@@@....@...@.@@@@..@@@.@.@.@@@.@..@@.@.@@@@.@@.@.@@@
+@.@.@.@@@@@@@@.@@.@@@.@@@..@@.@@@@@..@..@@@@@@@@....@.@@.@@@.@.@.@@@.@@..@@.@.@.@@.@..@.@.@.@@@@@.@@@..@.@@..@..@@@@@@@@....@@@@@..@.@...@.
+@@@@@@@@@@...@@@@@@.@..@..@.@..@@@@...@@.@.@@@@@.@@@@.@@@.@@..@.@@.@..@@@@..@@..@..@@@@@....@@.@.@@@@.@.@@...@..@@@@.@@...@@@@.......@@@@.@
+.@@@..@@@@@@.@@@.@.@.@@..@@@@..@@@@@@@.@@.@@@@...@@.@@@.@@@@.@@.@.@.@@@...@@..@@@@@..@@..@.@@@.@@.@@.@@@@@@...@.@@.@.@@.@.@....@@.@@@@@.@.@
+...@@.@@@@@@@.@@@@@@@@@@@@@.@.....@@@@.@@@.@@.@.@@@..@.....@@@@..@@@@@@...@@@.@..@.@..@.@.@@@@..@@@@@...@.@@@@.@@@@.@@@@.@@@.@.@@@@@.@...@@
+@@@..@@@@@@@@@@.@@@@@@..@@@...@@@@@.@@@....@@@..@..@@.@..@@..@.@...@..@@.@@@.@@@@@@.@.@@@@.@....@@@@@@@@..@@@@.@@@.@@@.@@..@@@.......@..@@@
+@@.@@@.@@..@.@.@@@@@.@.@@@@@..@.@@@.@@@@.....@.@@@.@@...@..@@@@.@.@@@@@@.@.@@.@@.@@@@@@@.@...@@@.@@@..@@@..@..@@..@@@@.@.@@@.@@@@@..@@..@@@
+@@@.@@.@@..@@@@@@.@.@@.@@@@@@..@@.@@@..@@@@@@@.@@@@..@@@@@@.@.@@@@@@@.@@.@.@@@@@.@...@@@@.@.@.@@@@@.@..@@@.@@@@@@.@@@@@@@.@.....@@..@.@..@.
+@@@.@@@@@@@@..@@@.@@@@.@@@.@@@.@@@.@@.@@@@.@@.@.@@@@@.@@@@@@@@.@@@@@.@@@@@@@@.@...@.@.@@.@@@@.@@.@@@.@@@@@@.@.@@@.@@...@@@@@@...@@.@...@.@@
+@@..@@....@.@@@..@@@.@@@@.@@@@@@.@@.@.@.@@@@@.@.@@@@.@@@@@@@@@@.@..@@@@.@@@@@@@@.@.@@@@@.@@..@@@@@@@.@..@@@.@@.@.@.@.@@@@@@.@.@.@@.@@@.@..@
+@@.@@@.@.@.@@..@@.@@@.@.@....@@@@@.@.@@..@..@@...@@@@@@..@..@.@@@@@.@@.@.@....@.....@@...@@@@@@@.@@@@@@@@@@@@.@@..@..@@..@@@.@@..@@.@.@.@..
+@.@@@@@.@@@@@@@@@@@.@@@@.@.@@@..@.@..@.@@@..@@.@@..@.@@..@.@..@@@@@..@@@@.@.@@...@.@@@.@@@@@@@@..@.@@@@..@@@..@.@@.@.@@.@.@.@@@@@@....@...@
+@@@@.@..@@@.@@.@@@@@@@@.@@@.@@@..@@..@@@.@@@.@@.@@@@@.@...@@@.@.@@.@.@.@@.@@..@..@@..@..@@@....@...@..@@@..@..@..@.@@@@@@.@.@@@.@@@@@@...@@
+@.@@@@.@....@@@.@@..@@.@@@@@...@@@@@.@.@@@..@@@@.@@@@.@@.@@@.@@@@@@.@@.@@@.@@@@@@@@@@@.@..@@..@@@.@..@@@@.@@@@@@@@@@@@@@@@.@@.@@@@@.@..@@@.
+@@@@@@@.@..@@@@@@@.@@.@@@@@@@.@@@.@....@@@@@@@..@@..@@@@@@.@.@@@@.@..@.@.@@.@@@..@@@@@@@@@@..@@..@@@@.@@@@..@@@@.@.@@@@@.@@..@.@@@.@@@@@@@@
+@@.@.@@@.@@.@.@.@...@..@.@...@@@@@@@@..@@@.@.@@.@..@.@...@@@@.@@@....@@@@@@@@..@@@@.@@@@@@.@@@@@..@...@..@.@@.@@@@@@@..@.@@@@@@@@@@..@..@@.
+@@@@.@@..@.@@@@.@..@.@@...@@@.@@....@.@.@.@..@.@@@@@.@@@@@.@@@..@@@.@@@.@@@.@@@@..@@.@.@@.@@@@@@@@.@.@@@@.@@@@@@@.@@@@.@.@@@.@@..@@@@@.@@@@
+@@@@.@@@@..@@@@@@@..@@@@@@@.@@@@.@..@@..@@.@@.@@@@.@@@@@@@@.@@.@@@@@@@@.@@..@.@.@.@@@.@@@.@@@.@.@.@@.@@@@@.@@@..@..@@@..@@..@...@@.@.@@..@@
+.@@@@..@@.......@@.@@@@@@@@.@@@.@@@@@@@....@.@@..@@.@@..@@@@@@...@@@@..@@@@@@@..@@@.@@.@@@...@@@...@..@@@.@.@..@..@@@@@@..@@@@@.@.@.@@@@@@.
+@@@@@@...@.@@@@..@@@.@@@@@@@@.@@.@@...@.@@@@@@.@@.@@...@@.@...@@@.@@.@@@.@@@@@.@.@@@@.@@...@@...@@..@@@@.....@@@@@@..@@@@@@@@@.@.@@@@@@.@@@
+@..@@.@@.@@@@@@.@@@@.@@...@@@@.@.@@@..@..@@@..@@@..@@..@.@@@@@@@@@..@@@@@@.@@.@@.@.@.@.@.@.@..@@@..@@@@@..@@@@@@@@@@@@.@.@@.@@@@@@@@...@@@.
+@@@.@@@.@...@@.@@..@@..@@@@....@@@@@@....@@.@@.@@@@@.@@@...@@@@..@..@...@@@@@@@.@@.@.@@@@@.@.@..@.@@.@.@@.@@@@@@.@@@.@.@.@@@@@....@.@@@@@.@
+@@@@@@@.@.@@@..@@..@@.@@@@.@..@@.@@.@@.@@@@.@@@@@.@@@@.@.@..@....@@..@@@@@@@.@@@@@@@@@@@@@........@@@@@...@@.@@@@@@@.@@@@@@..@@@@@@.@..@@.@
+.@@@@..@.@@.@@@.@@...@..@.@@@@@.@@@@..@@@@@.@@@@@.@..@@@@..@..@@@.@@@.@@@.@@@..@@@.@...@.@@@.@..@.@@@@@..@.@@.@.@@@@..@@@@@@@@@@.@.@.@.@@.@
+..@@@@..@.@@.@@@@@.@@..@.@..@@.@..@@@@@@.@.@..@@..@@@@.@@.@.@@@@.@.@@@.@@@@.@.@@@@@@@.@...@..@@..@@@@.@@@@@..@.@@...@@@.........@@@@@@..@@.
+@@@@.@.@.@@..@.@@.@@@@@@@..@@@@@.@.@@@@.@@@.@.@@@@@@@.@@@@@.@@....@.@@@.@..@..@@@@@.@@@@@@.@@@@.@@@..@@@.@@.@@@@.@.@@@@.@@.@@..@@@@@@@@@@@@
+@@@@@.@@....@@@@.@...@...@@@.@@@..@.@@@@@@@@.@@@@.@@@@.@@@@.@@@@@@@.@.@@...@.@...@...@.@@@.@@.@@..@@@@@@.@.@.@.@@..@@.@@@@@@@@@@..@...@@@@.
+.@@.@..@@@@@.@..@@@@@@@.@@.@..@.@@@@@.@@@@@@@@@@@@@@@@@@.@.@@@@@@.@@@@@@@@@@@@.@@.@@@.@..@@.@@.@@@@...@.@@..@.@@@@.@@@@@.@@@.@.@.@@@..@@@@.
+@@..@@....@@.@.@@.@@@@.@@@...@.@@@@@@.@@@.@@..@..@@@@@@@@@.@@@..@@@@@@@@@@.@.@.@..@@@@@@@@@@@@.@@@@@.@..@.@@.@.@@.@@@@@@.@@.@.@@@@@@@@@@@@.
+.@@..@@@@.@@@@.@@.@@.@@@@.....@@@@@.@@.@.@@.@..@@.@@@@@@@@.@@@@.@.....@.@.@@..@@.@@.@@.@@@@..@@@@.@.@@@@@@@@.@@@@@@@@.@@@@@@@@@@.@@@@.@@@.@
+@@@@@@@@@@.@@@@...@@..@@@@.@.@@@@.@.....@@@@.@....@.@@@@..@@@@@.@@.@...@@@@.@@@.@.@.@@@.@.@@.@@.@.@.@@@@@@@...@@.@@@..@@@@@@.@@.@..@@@.@@@@
+.@@@.@@@..@@........@.@@.@@..@@.@@@@.@@......@.@.....@..@@@..@@@@@@.@....@.@.@@@...@.@@@@..@@@@@.@@@@@@@@@@.@@@@@@@@@@@@.@@.@.@@..@@@.@.@@@
+..@@@@@@@.@..@@@.@@....@@.@@.@@.@@@@@@.@@@@..@@@@@@.@@@.@@@.@.@@.@@@@......@@@@..@@@@.@@@@@.@.@...@@@@@.@..@.@.@@@@@@@@@@@.@.@@.@.@@.@@@@@@
+...@.@@@.@...@@@@......@@@@@@@@@.@@@.@@@@@@@.@@@.@@@..@@.@@.@@..@.@@@@@@@@@.@@@@@@.@@@@@@.@.@@.....@@.@@...@@@@@....@@@.@@@.@.@@@..@@@@..@.
+...@..@..@@..@.@@.@@@@@@@@@..@@@.@@@@@@@@@@.@@@...@..@@@@@.@@@.@....@@.@.@...@.@@@@@@@@.@.@@..@@...@@..@@@..@@.@@@.@@.@@.@@@@@.@.@@..@.@@@@
+@@.@@@....@@@@@@@@.@.@@@..@@.@@@@.@@@@@.@.@@@..@.@.@@.@...@.@@..@.@@@@@@@.@@.@@@@@@..@.@.@@.@@@@.@.@@@@@@@@@@@@...@@@@.@@@@@...@.@@@..@.@@@
+..@.@@@.@.@..@@@.@...@@@.@@@@@@@@@@..@@@@@.@@.@@@.@@@@@@@.@..@.@@@.@....@@@@@@@@@@@.@..@@@@..@.@.@@@.@@@...@.@@.@..@@@@.@@..@@@...@.@..@@@@
+@@@@@@@@@.@@@@@@@@.@@.@@@@@@..@@@..@.@.@@@@@.@@@@@.@.@@@.@@.@@@@.@.@..@@@@@.@.@.@..@@@@@@@.@@.@.@@@@.@@.@@@@...@......@.@@.@@.@@..@.@@@@@@.
+.@@.@.@@@@@@...@.@@.@@.@@@@@.@@@@..@@@.@.@..@@@.@...@.@@@@@@@@@@...@.@..@..@@@@@@@.@..@@@@.@@.@..@.@@@@@@.@@@@@@@.@@@@@@...@@@.@@.@@@@@..@@
+@@@.@@....@@.@.@...@..@@.@.@@.@@...@@@...@@.@@@@.@.@@@@@@@@@@.@@@@@@@@@.@..@@@@..@.@@.@@@@.@@@..@@@@@.@@@@..@..@..@@.@@@@@@@@@@@@@@.@@@.@.@
+@..@@..@@..@@@@@@..@.@@.....@@..@@@...@@@@.@.@.@@@@@@.@@@@.@@....@@..@@@@@.@.@.@.@....@..@@.@@@@.@..@....@@.@.@@@@@@@@@....@@@@@@@@.@@@...@
+.@@@@.@@@@@.@.@.@@@..@@@...@@.@@@@@@@@@@@.@@@@..@@.@@.@@@@@@.@@@@@.@@@.@.@@@@@@.@.@..@@@.@@@@@@@.@.@@@..@.@@@...@@@.@@..@@@.@@@...@..@.@@@@
+.@.@.@@..@@.@@@.@.@@@@@@@@.@@@@@@@@@@.@.@@@.@.@@..@@..@@@.@....@@@.@@.@@@.@@@@@@@@@...@.@..@.@@@..@@.@@@.@@@.@@@.@@@@@.@.@@..@.@@..@@.@@@@.
+@.@@.@.@..@@..@@@@@@@.@@.@@..@@@@@...@@@@@.@@@.@.@.@@.@.@..@@@@.@@.@@@..@.@@@@@@@@@@@@..@@@@@.@...@.@@@@.@@@@@...@@.@.@@@@@@@@..@@@@....@@.
+.@@..@..@@@@@@.@@@@..@@@.@@@@@...@@.@@@.@.@...@.@.@@..@@@@@.@@.@.@...@....@...@@@.@@.@.@.@..@.@@@.@.@@..@.@.@.@@@@.@..@....@@..@@.@@@...@@.
+.@@...@@.@@@.@.@@@@.@@@@@.@@.@@@...@@.@@@@.@@..@@@@....@@@..@....@.@@@.@@@@@.@.@@.@@@.@@@..@@@@@@@@@@@@..@@@.@@..@@@@@@@.@.@.@.@@@@@@@@@@@.
+.@@@..@@@@..@@@@@@.@@.@..@@.@@@..@..@@.@@@@@@...@@@.@@...@@.@@.@@@.@@@@.@@@@@@@@@@.@@..@.@@@.@@@@.@@.@@@@..@@.....@@...@@@@.@..@@.@@@...@@@
+@@@..@@@@..@@.@@@@@....@@@@@@.@.@...@@@@@@@@.@.@@@@@.@@.@@@.@@@@@@@@@@..@..@.@.@@..@.@.@@@@....@@@.@@.@.@@@@.@..@@.@..@..@.@@@@@@@...@@@@@.
+..@@@@@@@.@@@..@@..@..@@@.@.@@.....@@.@@@@@@@.@@.@@.@@@@@@@@@@@.@@@.@..@@@@.@@@@.@..@@.@..@.@...@@.@@@@@@@@@..@@@@@@.@.@@@.@.@.@.@...@.@...
+@@..@.@@@.@@@..@@.@@@@@@@@.@.@.@.@@.@.@@@@@.@@@@.@@.@@@@.....@@@@@.@...@@@..@.@@@.@@.@.@@@@.@.@.@@.@...@..@..@.@.@.@@@@@@@@@.@@@...@@@@..@.
+.@@@@@..@.@@@@@@.@@@@.@@@@@@@@@@@@..@.@...@@@@.@@.@@.@@@.@@@.@.@@@..@@@..@.@@@@@@.@.@@@@@..@.@..@@@@@.@@@@@..@@@..@.@..@..@@@.@.@.@.@@....@
+@@@@@...@..@.@.@@.@.@@@@@@..@@..@@@@@.@.@@@@@@.@@@@@@@..@@@@@@@@@@@@@@@.@.@@.@@@.@@.@@@.@@@.@@@..@@@@.@.@@@@.@@@.@@.@.@@.@@@@..@...@.@..@@@
+....@@.@@@@@.@@@...@@@@.@@@.@.@.@.@@@.@@@.@@@@@@@@@@..@..@.@.@.@@.@@@@@@.@...@.@..@....@@@@@@@@.@.@..@@..@@@@@@@.@.@@.@@@@.@..@.@@..@@@@@..
+@@@.@...@@.@@.@@.@..@@.@@@.@@@@@.@@.@@@.@@@..@@@@@.@@.@@..@@@@.@@@@@@@.@@.@@@@@...@@@@.@....@@.@@@.@..@@.@.@.@.@@@.@@.@@..@@@.@@.@@@@@@@@@.
+@@.@.@@@..@.@.@@..@@@@.@@@.@..@@@..@@@.@@@@.@@.@@@@@..@...@@@@.@@@@.@@@@@...@.@@..@@..@@.@@.@.@..@@.@@.@.@...@...@..@@@.@@..@@@@@@@@@...@@@
+@@@@@.@@@@.@@@..@.@.@.@@@.@@..@.@@.@.@..@@.@@.@@@@@.@.@....@.@..@@@@@.@@@@@@@@@@@.@.@@.@@@.@@@@@@@.@@.@@..@@@@@.@@@@@@.@@@..@@@.@@@.@@@@.@@
+@@@@@.@.@@@.@.....@@@.@@.@@@@@..@..@@@@@.@@..@.@..@@@@.@@@@.@@....@@@.@.@@@.@...@.@@@@@@.@.@@@@@@.@@@..@.@.@@@@.@.@..@@@@@@.@@@@@@@.@.@@..@
+.@@@@..@@@@.@@@@@@@@..@.@.@@@.@.@@@@..@....@...@.@@@@@@@@...@.@.@@.@@.@.@.@@..@.@@.@@@..@@..@@.@..@@.@@@@@@.@@.@@@@@.@.@@@@@.@@@.@@@@@@.@@@
+@@..@@.@@.@@.@@.@.@.@@.@.@@.@@@@@.@@@....@.@.@@@@@@..@@@.@@@....@.....@@@@..@@@@@@.@.@@@@@@@@...@.@@..@@@@.@@..@..@@@@@@@@@..@@@.@@@@@@@.@@
+.@@.@@@@@@@@@@@@@@@@.@...@@..@@.@@@.@.@@@@@.@@@.@@..@@..@.@.....@..@....@@@@.....@.@@.@.@@@@@@.@@@@..@@@@@...@@@@@@@..@@@.......@...@@.@@@@
+@@@@.@.@@@.@@@@.@@@.@.@@@@@@@@@@@..@@@@.@.@.@.@@@@..@.@.@@@@.@@.@.@@@..@.@@.@....@.@@.@.@@...@@@.@@.@@.@@@@..@.@@@@@@.@@@..@..@@.@@..@.@@@@
+.@@@.@....@@..@@@@...@@@.@..@@@@@@@.@@@@@@.@..@@@@.@@@..@@@@@@.@@...@@@.@@@@@....@@..@@...@.@@@@.@@@@@@@.@.@@@@@....@@..@.@@@@@.@.@.@@@...@
+...@@@...@..@@@..@@..@@.@@.@.@@@@@.@@@@@@@@.@..@@@@@.@@@.@.@@..@@..@@...@@@@@.@@@@..@@@...@@@@@@@@@@@@.@@@@@@@@.@@@.@@@@..@@.@@...@@..@..@@
+@..@.@@.@.@@.@@@.@.@.@.@@..@@@@@@.@.@@@@@@@@..@@@@.@@...@.@..@@.@.@@.@..@.@@.@@@@@@.@@@..@.@..@@.@@.@@.@..@.@@..@@@@@.@.@@@...@.@@@@@.@@.@@
+@@@@..@@.@@@@@@@@@@.@.@@.@@@.@@@...@@@@@@.@@@..@@@@@@@.@@@@@.@@@@@@@.@@@.@@@@..@@@.@@@.....@@@..@@@.@..@@@@@@.@.@@....@@@.@@@..@@...@.@.@@@
+..@.@.@.@..@@@@...@.@@@@@@@@.@..@@.@@@@@@@@@@...@@@@@@.@@.@@@@@@@@@@..@@@@@@.@@@@@@@@@@@.@@@@@@@.@.@.@@@@..@@@@@@.@@.@@.@@.@.@@@@@@@@..@@@@
+@@..@@@@@@@@@@@@..@.@@@@@.@@@.@@@@@.@@@@..@@@.@@@.@@..@@@@.@....@@.@@..@@@@@@@@@@.@@@@@.@.@@.@@@@@@..@@@@@@.@@@@@.@@.@@.@@@..@@..@.@.@..@@.
+@.@@..@.@@@@.@@@...@.@@@@@.@@@.@.@@@@.@.@@@.@@.@@@.@@@@@.@..@.@@@@@@@.@@.@.@@.@@@@.@@@@@@@.@@@@@@@@.@.@@.@@@@@@@@@@.@.@.@@.@@.@.@@@@@@@@@@@
+@.@@@@@@.@@.@@@.@@@.@.@..@@@@@@.@@.@@@@@.@@@...@@@@@@@@@@@.@@..@@@@.@@.@@@@.@@@@@@@@.@@..@@@@@@..@.@@@@@@..@@@@@.@@@@@@.@..@.@.@@@.@.@@@.@@
+@@@@@@@@@@.@@@@@.@@@..@.@.@.@@@@.@@@.@.@@.@..@@@.@@@@@@@.@@.@@@@@@@@@@.@..@@..@.@@@.@@@@.@@.@@@.@.@@@@@.@@@@@..@..@@@@@@@..@@@@....@.@@@..@
+.@@.@..@.@.@@@@@...@@..@.@@@...@@@@@@..@@@.@@.@@@.@@@.@..@@@@.@...@@@@@.@@@@..@@.@@@.@@@@@@@@@@@@@@@@@.@.@.@@@..@...@.@@@@@.@.@@@@@@@.@.@.@
+..@@@...@@.@@@@@@...@..@@@@@@@...@@@@@.@..@@@@@@@@@@@@.@@@@@.@@.@@.@@@.@.@@.....@@@....@.@@@@...@.@@@..@.@@@@..@.@@@@@@@..@@@.@.@@@@@@@.@@.
+@@@@@@@@@...@@@.@@.@@..@@@@@...@.@@@..@@@..@@@.@@@@..@@.@@@@..@@@@@@@@@.@@@@.@@@@@.@@@..@@.@@@@.@@@@.....@@@@@@@@@@@.@@@..@@@@.@@.@@.@@@@@@
+@.@@@@@@@@..@..@@@.@..@@..@.@@@@@@@@@@..@@@.@.@@.@@..@.@@@@.@.@@@.@@@@.@@@@.@.@@@@.@@.@@@@@@.@@.@@@.@@.@@@@.@.@@@.@@.@@@@@@.@.@@.@@@.@@.@@@
+..@@.@@@.@@@@@@.@.@.@....@@...@@@.@.@@@@@.@@@@@...@@@@@@@.@@@@@.@@@.@@.@.@..@...@@@.@@@@@@.@@@@.@@@@@@@..@@@..@@@@..@@.@@..@@@@@@@@.@.@.@@.
+.@.@@@@@@@@.@..@@.@@@.@@..@.@..@@@@@.@@.@....@@..@@@.@@@@.@@.@@...@@@.@@@@@@..@.@@.@@..@@@.@.@@@.@@@@@@@.@@.@@...@.@..@@..@@@@@@@..@@...@.@
+@@@@@..@@@...@@.@.@@@@@@@..@@@..@@.@@..@@@@@@@@@..@@.@@@@.@...@...@..@@@.@.@@@@@@@@@@.@.@...@@..@@@@@@.@@@@@@@@@.@@@@@@@.@..@.@.@@@@@@.@@@@
+@.@..@@@@@..@@@@@@..@@@..@@@.@.@@@@@@@.@..@..@.@.@@.@@@..@..@@@@..@@@.@@@@@@.@@@@@..@.@.@@@...@@@@.@@@......@@.@@@.@..@.@@@@.@..@..@@.@@@@@
+@@..@@@@@@@@@@@@...@@@@@@@@@@@..@@@.@@@.@@.@@@.@@.@.@@@@.@@.@..@@@@@..@@@@@@.@....@@@@@@..@@..@@.@..@..@@@@@@@@@@..@.@@...@..@@@@@@@@....@@
+@@@@@@@..@.@.@.@.@@..@@..@@.@@.@.@@@..@..@@..@.@@..@..@@@@.@@@@.@@.@@.@@@...@.@@@@@@..@@.@@@@..@.@@.@@.@.@@...@.....@.@@@....@@@@@@..@.@..@
+.@.@.@@@@@@@@.@.@@@.@...@@@@@@@@.@.@@.@@@@@@@@.@@@@@..@@@@@@@.@.@.@@.@@@@@@@@@.@@@@@@@@..@.@...@.@@@@.....@@.@@@..@.@@@..@@@@@.@@@@@...@@.@
+@@..@@.@@@.@.@.@@..@...@@@.@@@.@@.@..@..@@@@..@@.@@.@@@@@.@@@...@@@..@@.@....@.@.@@.@@@@@@@@@@@@...@.@@@@@@@.@..@@@.@@@.@..@@@@@@.@@@.@@.@.
+....@@@@@@@@@..@.@@@@@...@.....@@..@@@..@@.@.@@..@@@@.@@.@@@@@@.@......@@.@@@@@..@.@@.@@@.@@@..@@@@..@@@@@@...@.@.@.@@..@...@@.@@@@..@@@@@.
+@@@@@@@.@.@@@@@@@@.@@@...@@@@@@@@..@@...@.@@.@@.@@.@@@.@@@@@@.@.@@.@.@.@@@@.@@@...@@@@@@..@@@@@@@.@...@@@@..@...@@@@.@.@@@@@..@.@@@..@@.@.@
+@.@@@...@.@@@.@@@@@.@@.@...@.@@@@@@.@@@@@@.@..@@.@@@@@@@@@@@@@@@.@@.@@@@......@.@@.@@@..@..@@@@....@@@@@@@@@@@@@.@@.@@@..@@@...@@@.@@..@@@.
+@.@@@@@.@@@.@@@.@..@@@@@@@..@@@.@@@...@@.....@@@@..@..@@@.@...@@@@..@..@@@@..@..@@..@@.@.@@.@.@@@@.@.@@.@...@@@@.@@@@@.@.@.@@@@@@.@@.@@@@@@
+@@@@@@@@@.@..@..@@..@@@@@@@.@@.@.@@@.@@@@.....@@@@.@@@.@@...@.@@.@@..@....@.@@@@@.@.@@@@@@@@@@@.@..@@.@@@@@@@@..@@@.@.@@.@@@@@@@@@..@@..@.@
+@..@@@@@@@@.@@.@@@@@.@@@.@..@@@.@@.@@...@@@@.@@.@.@..@@.@.@@@...@@@.@@.@@.@@@@@@.@@@..@.@@.@.@@@@@...@@@@.@@@@.@.@@..@..@..@@@@.@.@.@@.@@@@
+..@@.@@@@@@@@.@...@@@@@.@@@@@.@.@..@@@@@.@@@@@@@@@@.@@.@.@@@.@@.@@@@.@@.@@@.@.@@@@@@.@@@@..@.@@....@@@.@.@@.@@.@..@@@@..@.@@.@@.@...@@@@@..
+@@@@@@.@@@@@@@@@@@...@@.@@@@@@@...@@@.@..@....@..@@.@.@@@@@@@@@@@.@..@@.@.@@@@@@@@...@@..@@@.@@@.@...@@@.@@@@@@..@...@.@.@@..@.@@@@@.@@@@@.
+.@@@@.@@.@.@.@@@..@@@@...@@.@.@@@@.@@@..@@@.@@@@@@....@.@@@..@.@.@@@@@.@@.@.@@.@@@@@@@@..@@@.@..@.@@@..@@..@@.@@@@@.@@@@@.@.@@.@.@@.@@@.@.@
+..@@@@.@.@@..@@@@@.@@@@.@.@@@@@.@.@..@.@....@@@.@@@@@@.@.@@@...@@@@.@@@..@.@@@@@.@@.@@@@...@@.@.@.@.@.@@@@.@@..@@..@@....@..@@@@@@.@.@@@.@.
+.@@.@.@@.@@...@@@@@@@.@@.@.@@.@@@@@@.@.@@@..@@@@..@@@@.@.@@.@@.@@@.@....@@.@@.@@@@@@.@.@.@.@@@@@@@.@@@@@@.@@.@.@@.@...@@@.@@.@.@.@@@@..@.@.
+@.@@.@@@..@@@@@@..@@@.@@..@@@..@@@@.@@@.@@@.@.@@@@@.@@@@.@@@@@.@@@.@@@@@.@@@@@.@.@@@@.@@..@.@@@@@@@.@@@@.@.@..@@@@@..@@@@.@.@.@.@@@@@@@@@@.
+.@..@@.@@@@.@@..@@@@@@.....@@.@@@@.@@@@@@.@.@.@@@.@@@@@.@@@@.@@@.@@@..@.@@@.@.@.@@..@@@.@@.@@...@@@.@@@..@.@@@@@@@.@@@.@.@@@@.@@@@...@@.@@.
+@@.@@@@...@@@.@@@@@@@@@@.@@..@@.@@@.@@..@.@@..@@@@@.@@@@@.@@@@@.@.@@@@@..@@@.@@..@..@.@@@..@@.@.@@@.....@.@@@@@.@@...@@@.@@@...@@.@@@@.@.@@
+.@@.@@@.@@@.@@..@.@@.@.@@@.@@@..@@@.@@@..@...@@@.@@@@.@@@.@.@....@@.@.@@@@@@@@@@@@.@@@@@.@@@@.@@.@..@.@.@@@@@@.@@@@@..@@@@@@@...@@.@...@..@
+.@@@..@@.@@@@@.@...@...@@@@@@.@.@.@.@@@.@.@@.@.@.@....@@@.@@.@.@..@@@@.@.@.@@@.@.@@@@.@@@@.@@@@.@.@@.@.@@@@@@@@.@@@.@.@@.@...@@@.@@@.@@@@@@
+@@@@@@@..@@@....@@@@@.@@.@@.@@.@.@.@@.@@.@@@@.@@.@.@.@@@@.@..@.@@@.@..@@.@@@@@@.@@@...@..@.@...@@.@.@@..@.@.@@@.@@@.@...@.@.....@.@@@.....@
+@@@.@@.@.@@@.@@@@...@@@@..@.@..@.@@@@.@.@..@@@@@@@@@@@@.@@@.@...@@.@@@.@.@@....@@.@@@@@...@.@.@@@.@@.@.@.@@.@@@..@.@@@..@@@@@@@.@.@.@.@.@.@
+@@@@.@@@@@.@.@..@.@@.@@@@@@@.@@@.@..@@@@@@@@.@@..@@.@@@@@@@..@.@@.@@.@@@@@@@.@@@@@@@@@@@.@.@@...@..@..@@@@.@@@.@@@.@@@@@@@@@.@@.@.@..@@@@@.
+@@@...@@@@@@.@@@@@.@.@.@@@@@.@@@@@@@.@@@@.@@.@..@.@....@@@@..@.@@@@@..@.@@@..@@.@@@@@@.@@@@@...@....@@.@@..@.@.@@....@.@..@@.@.@@@.@@..@.@@
+.@@.@@@@.@.@@@.@@....@@@@@.@@@@.@@..@..@@@.@@@@@@@.@@@@......@.@@..@@.@.@@.@...@@@.@@.@.@@@@@@..@@@@@.@.@.@@@@@..@@@.@.@@@@@..@@.@@.@..@.@.
+@.@@@.@@..@.@@@@.@@...@@@....@@@@..@@@.@@@@@.@@@@@@.@.@.@@@@@.@.@@@.@@...@.@@.@@.@@.@@@..@@@.@@@.@.@@...@..@.@@@.@@.@@.@.@@....@@.@@.....@@
+...@..@@...@@@@@.@@.@@@@@@@@.@@@@@@.@.@.@@.@@@.@...@.@..@.@@@@.@.@@@@@@@@@@@@.@.@@@@.@@@@@@@..@@..@@.@@@@@.@@@.@@@@..@@.@@@@.@.@.@@..@@@@@.
+@..@.@@@@@.@...@.@@@@@..@@@@@@@.@@@@@@@.@@@@@@@@.@@.@.@@@@..@@@@@@@..@@@@@@@@@@@@@..@@@..@.@@@@@@@@@.@@@@@..@.@.@@@@@@@@.@@@@@@@@..@@...@@@
+.@@@@@@@.@@@.@.@@@.@.@.@@...@.@@.@.@@@.@@..@@@@@@@.@@..@@@@.@...@@@@.@@@@@.@@@@.@@@.@.@.@..@...@@@..@@@@@@@@@.@@.@@..@.@@@.@.@@@..@@@@.@.@.
+.@.@.@...@@@.@.@@.@.@..@@.@@.@..@@@@@@@..@...@.@@@@@@.@@@.@@.@...@.@@@@.@@.@@@@.@.@.@@@.......@@@...@@@..@.@@@..@...@@@.@..@@@@.@@@@@@.@.@@
+.@.@@@@@..@@@@.@.@@...@@.@@.@@@@@...@@@@@@@@.@..@@@@.@.@@.@@@@@@.@@.@.....@...@@@@@@@.@@@..@.@@.@@@@@@.@.@@@@@@@@.@@@@.@@@@@@@@...@@@@@...@
+.@@.@@...@@...@@@@@..@@.@.@..@@@@@@.@@@..@.@.@@@@.@@@..@@@@@@@@@@@..@@@@@@@@@@@@@@@.@@@.@@@@@@..@@.@.@@@@@@@@.@@@@@.@@.@@@.@.@@@@.@@@.@@.@.
+@@@@@@@@@@@.@@...@@..@.....@@@@@@@@..@..@..@@@@@@....@.@@.@@@..@@@@@@@@@.@@.....@@.@@...@.@...@....@@@@@@@.@@@...@@.@...@@.@.@@@@@.@@@@...@
+@.@@.@@..@@@@.@@.@@@...@@@@@@@@@@.@.@@@..@@...@@...@....@@@@..@.@@@..@.@@@@..@@@@@@@@@@@@.@@.@.@.@.@@..@@..@@@@..@.@@@.@@..@.@@.@@@@...@@@@
+@@.@@@@.@.@@.@@.@@@@@..@.....@@@@@@.@@@@.@@...@@@@@.@@@@@.@.@@@@..@..@...@@.@@@@@@@@@..@..@.@..@@.@.@@@@.@.@@.@@.@.@@@.....@.@@@@.@@@@@.@@.
+@@@...@.@@..@@@.@@.@@@@.@..@..@.@@@@@@.@@@@..@.@@@.@....@@.@@.@@@@@.@.@...@...@.@@@....@@@...@@.@@@@@@@.@@.@@@.@@@@@@@.@@@.@.@@@..@.@@...@@
+@.@@@@@@@@@..@@@@@@..@@@@.@@.@.@@@..@.@.@...@@@@@@.@@@..@.@@@@..@@@@@@@.....@@@@.@@.@@.@.@@@@.@....@@.@@@.@.@@.@.@.@.@@@..@@.@...@.@@..@@.@
+@@@@@@@..@.@@@@.@@..@@.@.@@@..@.@@...@@.@@.@@@@.@.@@...@@@.@@@@@@@..@@..@.@@@.@@@@@.@@@@@.@.@@.@@@.@@@...@@..@@@@@@@@@..@@@@..@@@@@@.@@@.@@
+..@.@@@@@@@@@@.@..@@...@....@@@.@.@@...@@@@@@.@.@@@@@@@@@@.@.@@@@@.@@@@.@@@@.@@..@@.@...@..@@...@@@.@.@..@@.@@@.@.@@@@.@@@@..@@@@.@....@@@@
+@@@.@.@.@@.@.@.@@@...@@@@@@@@.....@@@@.@@@@@...@..@@.@@.@@@...@..@@@.@@@@@..@@@.@..@.@@@@..@@@.@...@@..@.@@@@@.@@.@@..@@@.@@@@@@@.@@@@@@@.@
+@.@..@@....@@.@@.@.@.@@@@@..@@@@@.@@@...@@@@@.@@..@@.@@@.@...@.@.@@@@..@@.@.@@@@@..@..@@@@@@@@@@@@@.@@@@..@.@@.@.@@@@@.@.@@@..@@@@@@@.@@@@.
+...@.@@@@@.@@@@@@.@@@@.@@@..@@.@@@.@@@..@@@@@@@.@@...@.@..@@@@.@@@.@@.@@@.@..@..@@.@@@.@@@..@@.@@@.@@..@@.@@...@........@@...@@@@@@@@@.@@.@
+.@..@@@..@..@@@@...@@..@@...@@@..@.@@.@@@.@@@@@@@@@@.@@@@@..@..@@@@.@@@.@@@@.@@.@..@@@@@..@@@@@..@@@@.@@..@.@.@.@@@@@...@@@@@@.@.@.@@@@@.@.
+@@@.@.@@.@@@@....@.@@..@@.@@@@@.@.@@..@@@..@@.@@.@.@.@@.@@.@@@.@.@@.@.@@@@.@@@@@@@..@@..@@.@@@@@@@...@@.@.@.@...@..@@@.@@..@@@..@@.@@@@.@@@
+@@.@@.@@.@......@@.@@.@.@@@.@@@@.@@@@@@@@.@@@.@@@..@@..@@@@@..@.@@@@...@.@@@@@@@@@@.@@...@@.@@.@.@@..@@@@..@.@.@...@..@@@@@.@@@.@.@.@@@...@
+@@.@@@@@@@@@@.@@@@.@@@@..@@.@@@.@@@.@@...@@@.@@..@..@.@..@..@.@@@....@@..@@.@@@@@@......@@@..@...@@.@@@@..@@@..@.@.@@@.@@@@@@@.@@..@.@@@@@.
+@@@.@@..@@@.@@@@.@.@.@@.@@@..@..@@@@@...@@@@@.@@@@@.@@..@..@@@@.@@@@.@@@@@..@..@@@@@@@....@@@@@.@...@@@@@@@@@@@@..@@@@@.@..@@@...@@@.@..@@.
+.@....@.@@@@@@.@@.@@..@@@.@@@@.@@@@@@@@.@@..@@@@@@@..@.@@..@@.@....@.@.@...@@@..@@....@@@@@.....@@@@@@@@@@@@@.@@@@@.@..@.@.@..@@@@@@@@@.@@.
+.@@@@.@@@@.@@@.@@@@@.@..@@@.@@@@@@@@@..@.@@@..@@@@@@.@.@@..@@@.@@.@@.@...@..@@@@@@@.@@@@@.@.@@.@@.....@@@@@....@@.@@.@@@@.@.@@@@@..@@@@.@@@
diff --git a/Advents/AoC2025/day04.lean b/Advents/AoC2025/day04.lean
new file mode 100644
index 00000000..2fa16d4e
--- /dev/null
+++ b/Advents/AoC2025/day04.lean
@@ -0,0 +1,49 @@
+import Advents.Utils
+open Std
+
+namespace AoC2025_Day04
+
+open System in
+/-- `input` is the location of the file with the data for the problem. -/
+def input : FilePath := ("Advents"/"AoC2025"/"day04" : FilePath).withExtension "input"
+
+/-!
+#  Question 1
+-/
+
+/-- `test` is the test string for the problem. -/
+def test := "..@@.@@@@.
+@@@.@.@.@@
+@@@@@.@.@@
+@.@@@@..@.
+@@.@@@@.@@
+.@@@@@@@.@
+.@.@.@.@@@
+@.@@@.@@@@
+.@@@@@@@@.
+@.@.@@@.@."
+
+/-- `atest` is the test string for the problem, split into rows. -/
+def atest := (test.splitOn "\n").toArray
+
+/-- `part1 dat` takes as input the input of the problem and returns the solution to part 1. -/
+def part1 (dat : Array String) : Nat := sorry
+--def part1 (dat : String) : Nat := sorry
+
+--#assert part1 atest == ???
+
+--set_option trace.profiler true in solve 1
+
+/-!
+#  Question 2
+-/
+
+/-- `part2 dat` takes as input the input of the problem and returns the solution to part 2. -/
+def part2 (dat : Array String) : Nat := sorry
+--def part2 (dat : String) : Nat :=
+
+--#assert part2 atest == ???
+
+--set_option trace.profiler true in solve 2
+
+end AoC2025_Day04

From 8ede4876f55eb9e2935a72a4d2a907b2ffdc56de Mon Sep 17 00:00:00 2001
From: adomani <adomani@gmail.com>
Date: Thu, 4 Dec 2025 05:22:21 +0000
Subject: [PATCH 02/10] part 1

---
 Advents/AoC2025/day04.lean | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/Advents/AoC2025/day04.lean b/Advents/AoC2025/day04.lean
index 2fa16d4e..38003f64 100644
--- a/Advents/AoC2025/day04.lean
+++ b/Advents/AoC2025/day04.lean
@@ -26,6 +26,27 @@ def test := "..@@.@@@@.
 /-- `atest` is the test string for the problem, split into rows. -/
 def atest := (test.splitOn "\n").toArray
 
+instance : Add (Int × Int) where
+  add := fun (a, b) (c, d) => (a + c, b + d)
+
+def neighs (h : HashSet pos) (p : pos) : HashSet pos := Id.run do
+  let mut fin := ∅
+  for ns in [(1, 0), (0, 1), (-1, 0), (0, -1), (1, 1), (1, -1), (-1, 1), (-1, -1)] do
+    let new := p + ns
+    if h.contains new then
+      fin := fin.insert new
+  return fin
+
+#eval do
+  let dat := atest
+  let dat ← IO.FS.lines input
+  let gr := sparseGrid dat (· == '@')
+  draw <| drawSparse gr dat.size dat[0]!.length
+  let le4 := gr.filter fun p => (neighs gr p).size < 4
+  draw <| drawSparse le4 dat.size dat[0]!.length
+  IO.println le4.size
+
+
 /-- `part1 dat` takes as input the input of the problem and returns the solution to part 1. -/
 def part1 (dat : Array String) : Nat := sorry
 --def part1 (dat : String) : Nat := sorry

From b885276d538771f8d81aee52029f31f55a8efbee Mon Sep 17 00:00:00 2001
From: adomani <adomani@gmail.com>
Date: Thu, 4 Dec 2025 05:23:23 +0000
Subject: [PATCH 03/10] clean 1

---
 Advents/AoC2025/day04.lean | 27 ++++++++++++++-------------
 1 file changed, 14 insertions(+), 13 deletions(-)

diff --git a/Advents/AoC2025/day04.lean b/Advents/AoC2025/day04.lean
index 38003f64..1e714a9c 100644
--- a/Advents/AoC2025/day04.lean
+++ b/Advents/AoC2025/day04.lean
@@ -37,28 +37,29 @@ def neighs (h : HashSet pos) (p : pos) : HashSet pos := Id.run do
       fin := fin.insert new
   return fin
 
-#eval do
-  let dat := atest
-  let dat ← IO.FS.lines input
+/-- `part1 dat` takes as input the input of the problem and returns the solution to part 1. -/
+def part1 (dat : Array String) : Nat :=
   let gr := sparseGrid dat (· == '@')
-  draw <| drawSparse gr dat.size dat[0]!.length
   let le4 := gr.filter fun p => (neighs gr p).size < 4
-  draw <| drawSparse le4 dat.size dat[0]!.length
-  IO.println le4.size
-
-
-/-- `part1 dat` takes as input the input of the problem and returns the solution to part 1. -/
-def part1 (dat : Array String) : Nat := sorry
---def part1 (dat : String) : Nat := sorry
+  le4.size
 
---#assert part1 atest == ???
+#assert part1 atest == 13
 
---set_option trace.profiler true in solve 1
+solve 1 1409
 
 /-!
 #  Question 2
 -/
 
+#eval do
+  let dat := atest
+  let dat ← IO.FS.lines input
+  let gr := sparseGrid dat (· == '@')
+  draw <| drawSparse gr dat.size dat[0]!.length
+  let le4 := gr.filter fun p => (neighs gr p).size < 4
+  draw <| drawSparse le4 dat.size dat[0]!.length
+  IO.println le4.size
+
 /-- `part2 dat` takes as input the input of the problem and returns the solution to part 2. -/
 def part2 (dat : Array String) : Nat := sorry
 --def part2 (dat : String) : Nat :=

From a06f9a2c22ef0fd2acbf23c373ef30181c616539 Mon Sep 17 00:00:00 2001
From: adomani <adomani@gmail.com>
Date: Thu, 4 Dec 2025 05:36:20 +0000
Subject: [PATCH 04/10] part 2

---
 Advents/AoC2025/day04.lean | 22 +++++++++++++++++-----
 1 file changed, 17 insertions(+), 5 deletions(-)

diff --git a/Advents/AoC2025/day04.lean b/Advents/AoC2025/day04.lean
index 1e714a9c..ab8e4046 100644
--- a/Advents/AoC2025/day04.lean
+++ b/Advents/AoC2025/day04.lean
@@ -37,10 +37,13 @@ def neighs (h : HashSet pos) (p : pos) : HashSet pos := Id.run do
       fin := fin.insert new
   return fin
 
+def accessible (h : HashSet pos) : HashSet pos :=
+  h.filter fun p => (neighs h p).size < 4
+
 /-- `part1 dat` takes as input the input of the problem and returns the solution to part 1. -/
 def part1 (dat : Array String) : Nat :=
   let gr := sparseGrid dat (· == '@')
-  let le4 := gr.filter fun p => (neighs gr p).size < 4
+  let le4 := accessible gr
   le4.size
 
 #assert part1 atest == 13
@@ -55,10 +58,19 @@ solve 1 1409
   let dat := atest
   let dat ← IO.FS.lines input
   let gr := sparseGrid dat (· == '@')
-  draw <| drawSparse gr dat.size dat[0]!.length
-  let le4 := gr.filter fun p => (neighs gr p).size < 4
-  draw <| drawSparse le4 dat.size dat[0]!.length
-  IO.println le4.size
+  let mut old := gr
+  let mut new := old.filter fun p => 4 ≤ (neighs old p).size
+  let mut rems := old.size - new.size
+  IO.println (rems, old.size - new.size)
+  let mut con := 0
+  while old != new do
+    old := new
+    con := con + 1
+    IO.println s!"Step {con}"
+    new := old.filter fun p => 4 ≤ (neighs old p).size
+    --draw <| drawSparse new dat.size dat[0]!.length
+    rems := rems + old.size - new.size
+    IO.println (rems, old.size - new.size)
 
 /-- `part2 dat` takes as input the input of the problem and returns the solution to part 2. -/
 def part2 (dat : Array String) : Nat := sorry

From 893d28b9b329a208c223fb52cfd871487441d8a0 Mon Sep 17 00:00:00 2001
From: adomani <adomani@gmail.com>
Date: Thu, 4 Dec 2025 05:48:07 +0000
Subject: [PATCH 05/10] doc utils

---
 Advents/Utils.lean | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/Advents/Utils.lean b/Advents/Utils.lean
index 9a7f7b8a..44695d36 100644
--- a/Advents/Utils.lean
+++ b/Advents/Utils.lean
@@ -349,7 +349,12 @@ def drawHash {α} [ToString α] (h : HashMap pos α) (Nx Ny : Nat) : Array Strin
     fin := fin.push str
   return fin
 
-/-- A function to draw `HashSet`s. -/
+/--
+A function to draw `HashSet`s.
+
+The `Nx` input is the *vertical* span of the `HashSet`,
+the `Ny` input is the *horizontal* span of the `HashSet`.
+-/
 def drawSparseWith (h : HashSet pos) (Nx Ny : Nat)
     (yes : pos → String := fun _ => "#") (no : pos → String := fun _ => ".") :
     Array String := Id.run do
@@ -363,7 +368,12 @@ def drawSparseWith (h : HashSet pos) (Nx Ny : Nat)
     fin := fin.push str
   return fin
 
-/-- A function to draw `HashSet`s. -/
+/--
+A function to draw `HashSet`s.
+
+If `h` is obtained by reading a "grid" `dat : Array String`, then
+the `Nx` input is likely `dat.size` and the `Ny` input is likely `dat[0]!.length`.
+-/
 def drawSparse (h : HashSet pos) (Nx Ny : Nat) (yes : String := "#") (no : String := "·") :
     Array String := Id.run do
   let mut fin := #[]

From 91d50f2204fa3bf7954598767a357b4ee2e7df8c Mon Sep 17 00:00:00 2001
From: adomani <adomani@gmail.com>
Date: Thu, 4 Dec 2025 05:48:23 +0000
Subject: [PATCH 06/10] partial clean up, slow

---
 Advents/AoC2025/day04.lean | 25 +++++++++++++++----------
 1 file changed, 15 insertions(+), 10 deletions(-)

diff --git a/Advents/AoC2025/day04.lean b/Advents/AoC2025/day04.lean
index ab8e4046..52fcf977 100644
--- a/Advents/AoC2025/day04.lean
+++ b/Advents/AoC2025/day04.lean
@@ -37,13 +37,10 @@ def neighs (h : HashSet pos) (p : pos) : HashSet pos := Id.run do
       fin := fin.insert new
   return fin
 
-def accessible (h : HashSet pos) : HashSet pos :=
-  h.filter fun p => (neighs h p).size < 4
-
 /-- `part1 dat` takes as input the input of the problem and returns the solution to part 1. -/
 def part1 (dat : Array String) : Nat :=
   let gr := sparseGrid dat (· == '@')
-  let le4 := accessible gr
+  let le4 := gr.filter fun p => (neighs gr p).size < 4
   le4.size
 
 #assert part1 atest == 13
@@ -55,8 +52,8 @@ solve 1 1409
 -/
 
 #eval do
-  let dat := atest
   let dat ← IO.FS.lines input
+  let dat := atest
   let gr := sparseGrid dat (· == '@')
   let mut old := gr
   let mut new := old.filter fun p => 4 ≤ (neighs old p).size
@@ -68,16 +65,24 @@ solve 1 1409
     con := con + 1
     IO.println s!"Step {con}"
     new := old.filter fun p => 4 ≤ (neighs old p).size
-    --draw <| drawSparse new dat.size dat[0]!.length
+    draw <| drawSparse new dat.size dat[0]!.length
     rems := rems + old.size - new.size
     IO.println (rems, old.size - new.size)
 
 /-- `part2 dat` takes as input the input of the problem and returns the solution to part 2. -/
-def part2 (dat : Array String) : Nat := sorry
---def part2 (dat : String) : Nat :=
+def part2 (dat : Array String) : Nat := Id.run do
+  let gr := sparseGrid dat (· == '@')
+  let mut old := gr
+  let mut new := old.filter fun p => 4 ≤ (neighs old p).size
+  let mut rems := old.size - new.size
+  while old != new do
+    old := new
+    new := old.filter fun p => 4 ≤ (neighs old p).size
+    rems := rems + old.size - new.size
+  return rems
 
---#assert part2 atest == ???
+#assert part2 atest == 43
 
---set_option trace.profiler true in solve 2
+set_option trace.profiler true in solve 2 8366
 
 end AoC2025_Day04

From 0e92b32a543b87f6a4e650b217c057f2a4464613 Mon Sep 17 00:00:00 2001
From: adomani <adomani@gmail.com>
Date: Thu, 4 Dec 2025 06:29:34 +0000
Subject: [PATCH 07/10] speed up

---
 Advents/AoC2025/day04.lean | 42 +++++++++++++++++++++++++++++---------
 1 file changed, 32 insertions(+), 10 deletions(-)

diff --git a/Advents/AoC2025/day04.lean b/Advents/AoC2025/day04.lean
index 52fcf977..01f9f72a 100644
--- a/Advents/AoC2025/day04.lean
+++ b/Advents/AoC2025/day04.lean
@@ -26,9 +26,6 @@ def test := "..@@.@@@@.
 /-- `atest` is the test string for the problem, split into rows. -/
 def atest := (test.splitOn "\n").toArray
 
-instance : Add (Int × Int) where
-  add := fun (a, b) (c, d) => (a + c, b + d)
-
 def neighs (h : HashSet pos) (p : pos) : HashSet pos := Id.run do
   let mut fin := ∅
   for ns in [(1, 0), (0, 1), (-1, 0), (0, -1), (1, 1), (1, -1), (-1, 1), (-1, -1)] do
@@ -51,21 +48,39 @@ solve 1 1409
 #  Question 2
 -/
 
+def getNbs (h rem : HashSet pos) : HashSet pos :=
+  rem.fold (init := ∅) fun tot p => Id.run do
+    let mut here : HashSet pos := ∅
+    for n in [(1, 0), (0, 1), (-1, 0), (0, -1), (1, 1), (1, -1), (-1, 1), (-1, -1)] do
+      let shifted := p + n
+      if shifted ∈ h then here := here.insert shifted
+    tot.insertMany here
+
 #eval do
-  let dat ← IO.FS.lines input
   let dat := atest
+  let dat ← IO.FS.lines input
   let gr := sparseGrid dat (· == '@')
   let mut old := gr
-  let mut new := old.filter fun p => 4 ≤ (neighs old p).size
+  let mut (new, removed) := old.partition fun p => 4 ≤ (neighs old p).size
+  let mut nearRemoved := getNbs old removed
   let mut rems := old.size - new.size
+
   IO.println (rems, old.size - new.size)
   let mut con := 0
-  while old != new do
+  while old != new && con ≤ 55 do
     old := new
     con := con + 1
     IO.println s!"Step {con}"
-    new := old.filter fun p => 4 ≤ (neighs old p).size
-    draw <| drawSparse new dat.size dat[0]!.length
+    --nearRemoved := getNbs old removed
+    let mut (new', removed') : HashSet pos × HashSet pos := (old, ∅)
+    for p in nearRemoved do
+      if (neighs old p).size < 4 then
+        new' := new'.erase p
+        removed' := removed'.insert p
+    (new, removed) := (new', removed') --old.partition fun p => 4 ≤ (neighs old p).size
+    nearRemoved := getNbs old removed
+
+    --draw <| drawSparse new dat.size dat[0]!.length
     rems := rems + old.size - new.size
     IO.println (rems, old.size - new.size)
 
@@ -73,11 +88,18 @@ solve 1 1409
 def part2 (dat : Array String) : Nat := Id.run do
   let gr := sparseGrid dat (· == '@')
   let mut old := gr
-  let mut new := old.filter fun p => 4 ≤ (neighs old p).size
+  let mut (new, removed) := old.partition fun p => 4 ≤ (neighs old p).size
+  let mut nearRemoved := getNbs old removed
   let mut rems := old.size - new.size
   while old != new do
     old := new
-    new := old.filter fun p => 4 ≤ (neighs old p).size
+    let mut (new', removed') : HashSet pos × HashSet pos := (old, ∅)
+    for p in nearRemoved do
+      if (neighs old p).size < 4 then
+        new' := new'.erase p
+        removed' := removed'.insert p
+    (new, removed) := (new', removed')
+    nearRemoved := getNbs old removed
     rems := rems + old.size - new.size
   return rems
 

From 44b6c34e89dec646730a57d63dc5e5fa0d2e5b94 Mon Sep 17 00:00:00 2001
From: adomani <adomani@gmail.com>
Date: Thu, 4 Dec 2025 06:30:54 +0000
Subject: [PATCH 08/10] remove temp

---
 Advents/AoC2025/day04.lean | 30 +-----------------------------
 1 file changed, 1 insertion(+), 29 deletions(-)

diff --git a/Advents/AoC2025/day04.lean b/Advents/AoC2025/day04.lean
index 01f9f72a..32f99991 100644
--- a/Advents/AoC2025/day04.lean
+++ b/Advents/AoC2025/day04.lean
@@ -56,34 +56,6 @@ def getNbs (h rem : HashSet pos) : HashSet pos :=
       if shifted ∈ h then here := here.insert shifted
     tot.insertMany here
 
-#eval do
-  let dat := atest
-  let dat ← IO.FS.lines input
-  let gr := sparseGrid dat (· == '@')
-  let mut old := gr
-  let mut (new, removed) := old.partition fun p => 4 ≤ (neighs old p).size
-  let mut nearRemoved := getNbs old removed
-  let mut rems := old.size - new.size
-
-  IO.println (rems, old.size - new.size)
-  let mut con := 0
-  while old != new && con ≤ 55 do
-    old := new
-    con := con + 1
-    IO.println s!"Step {con}"
-    --nearRemoved := getNbs old removed
-    let mut (new', removed') : HashSet pos × HashSet pos := (old, ∅)
-    for p in nearRemoved do
-      if (neighs old p).size < 4 then
-        new' := new'.erase p
-        removed' := removed'.insert p
-    (new, removed) := (new', removed') --old.partition fun p => 4 ≤ (neighs old p).size
-    nearRemoved := getNbs old removed
-
-    --draw <| drawSparse new dat.size dat[0]!.length
-    rems := rems + old.size - new.size
-    IO.println (rems, old.size - new.size)
-
 /-- `part2 dat` takes as input the input of the problem and returns the solution to part 2. -/
 def part2 (dat : Array String) : Nat := Id.run do
   let gr := sparseGrid dat (· == '@')
@@ -105,6 +77,6 @@ def part2 (dat : Array String) : Nat := Id.run do
 
 #assert part2 atest == 43
 
-set_option trace.profiler true in solve 2 8366
+solve 2 8366
 
 end AoC2025_Day04

From 58a6b8dceab3e7c25d1074304a0ecb42c58afe84 Mon Sep 17 00:00:00 2001
From: adomani <adomani@gmail.com>
Date: Thu, 4 Dec 2025 06:34:20 +0000
Subject: [PATCH 09/10] docs

---
 Advents/AoC2025/day04.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/Advents/AoC2025/day04.lean b/Advents/AoC2025/day04.lean
index 32f99991..67867814 100644
--- a/Advents/AoC2025/day04.lean
+++ b/Advents/AoC2025/day04.lean
@@ -26,6 +26,10 @@ def test := "..@@.@@@@.
 /-- `atest` is the test string for the problem, split into rows. -/
 def atest := (test.splitOn "\n").toArray
 
+/--
+Finds the elements of `h` that are neighbours of position `p`,
+in one of the possible `8` directions.
+-/
 def neighs (h : HashSet pos) (p : pos) : HashSet pos := Id.run do
   let mut fin := ∅
   for ns in [(1, 0), (0, 1), (-1, 0), (0, -1), (1, 1), (1, -1), (-1, 1), (-1, -1)] do
@@ -48,6 +52,10 @@ solve 1 1409
 #  Question 2
 -/
 
+/--
+Given two `h rem : HashSet pos`, returns the `HashSet` of those elements of `h` that are
+neighbours of some element of `rem`.
+-/
 def getNbs (h rem : HashSet pos) : HashSet pos :=
   rem.fold (init := ∅) fun tot p => Id.run do
     let mut here : HashSet pos := ∅

From 2d6c6485a1882c401864d6de9f8906e5a6de284e Mon Sep 17 00:00:00 2001
From: adomani <adomani@gmail.com>
Date: Thu, 4 Dec 2025 06:37:12 +0000
Subject: [PATCH 10/10] add descriptions

---
 .src/2025_desc.txt                            | 14 ++++++++
 Advents/AoC2025/2025_descriptions.md          |  1 +
 .../AoC2025/2025_descriptions_with_tests.md   | 35 +++++++++++++++++++
 3 files changed, 50 insertions(+)

diff --git a/.src/2025_desc.txt b/.src/2025_desc.txt
index 04cfa5cf..e5a280d8 100644
--- a/.src/2025_desc.txt
+++ b/.src/2025_desc.txt
@@ -48,3 +48,17 @@ Their sum would be `55`.
 
 For the second part, we should do the same as in part 1, except that we want to sum the largest
 12-digit numbers that can be extracted.
+-- Day 4
+The input is a grid with the positions of rolls of paper.
+
+### Description
+
+#### Part 1
+
+We should find the number of rolls of papers that have fewer than `4` nearby rolls of paper.
+
+#### Part 2
+
+For the second part, we should recursively remove all rolls of paper that have fewer than `4` nearby
+rolls of paper, until no more rolls can be removed.
+We should report how rolls we removed in the process.
diff --git a/Advents/AoC2025/2025_descriptions.md b/Advents/AoC2025/2025_descriptions.md
index 415c77af..c0359164 100644
--- a/Advents/AoC2025/2025_descriptions.md
+++ b/Advents/AoC2025/2025_descriptions.md
@@ -3,3 +3,4 @@
 | [1](2025_descriptions_with_tests.md#day-1) | The input is a lists strings, starting with either `L` or `R` and continuing with a natural number. |
 | [2](2025_descriptions_with_tests.md#day-2) | The input is a sequence of ranges of IDs that are all natural numbers.                              |
 | [3](2025_descriptions_with_tests.md#day-3) | The input is a list of sequences of joltages, each of which is a natural number from `1` to `9`.    |
+| [4](2025_descriptions_with_tests.md#day-4) | The input is a grid with the positions of rolls of paper.                                           |
diff --git a/Advents/AoC2025/2025_descriptions_with_tests.md b/Advents/AoC2025/2025_descriptions_with_tests.md
index 5f706e84..d5e99d65 100644
--- a/Advents/AoC2025/2025_descriptions_with_tests.md
+++ b/Advents/AoC2025/2025_descriptions_with_tests.md
@@ -96,3 +96,38 @@ For the second part, we should do the same as in part 1, except that we want to
 [Solution in Lean](day03.lean)
 
 ---
+
+#  [Day 4](https://adventofcode.com/2025/day/4)
+
+The input is a grid with the positions of rolls of paper.
+
+####  Test
+
+<pre>
+..@@.@@@@.
+@@@.@.@.@@
+@@@@@.@.@@
+@.@@@@..@.
+@@.@@@@.@@
+.@@@@@@@.@
+.@.@.@.@@@
+@.@@@.@@@@
+.@@@@@@@@.
+@.@.@@@.@.
+</pre>
+
+### Description
+
+#### Part 1
+
+We should find the number of rolls of papers that have fewer than `4` nearby rolls of paper.
+
+#### Part 2
+
+For the second part, we should recursively remove all rolls of paper that have fewer than `4` nearby
+rolls of paper, until no more rolls can be removed.
+We should report how rolls we removed in the process.
+
+[Solution in Lean](day04.lean)
+
+---