diff --git a/.src/2025_desc.txt b/.src/2025_desc.txt
index 41cdd02..10f9852 100644
--- a/.src/2025_desc.txt
+++ b/.src/2025_desc.txt
@@ -123,3 +123,17 @@ Now, we should add all edges, from the shortest to the largest, until the graph
 connected component.
 Once that happens, we should report the product of the `x`-coordinates of the last edge that was
 added.
+-- Day 9
+The input are the coordinates of the red tiles.
+
+### Description
+
+#### Part 1
+
+In part 1, we should determine the largest area of a rectangle with two opposite corners
+on the red tiles.
+
+#### Part 2
+
+In part 2, we should still find the largest rectangle with opposite vertices on the red tiles,
+but the rectangle must be entirely contained in the interior of the path.
diff --git a/.src/todo.md b/.src/todo.md
index 4bf6454..4faf0cf 100644
--- a/.src/todo.md
+++ b/.src/todo.md
@@ -38,3 +38,4 @@
 
 ### 2025
 * Day 8: both parts are slow, the first one is only sped up by a hard-coded answer.
+* Day 9, part 2: missing -- finding rectangles in the interior of a region.
diff --git a/Advents.lean b/Advents.lean
index 70b9059..2e5bf6b 100644
--- a/Advents.lean
+++ b/Advents.lean
@@ -7,3 +7,4 @@ import Advents.AoC2025.day05
 import Advents.AoC2025.day06
 import Advents.AoC2025.day07
 import Advents.AoC2025.day08
+import Advents.AoC2025.day09
diff --git a/Advents/AoC2025/2025_descriptions.md b/Advents/AoC2025/2025_descriptions.md
index d32252d..f86e0ba 100644
--- a/Advents/AoC2025/2025_descriptions.md
+++ b/Advents/AoC2025/2025_descriptions.md
@@ -8,3 +8,4 @@
 | [6](2025_descriptions_with_tests.md#day-6) | Helping cephalopods with their maths homework                                                       |
 | [7](2025_descriptions_with_tests.md#day-7) | Splitting tachyon manifolds                                                                         |
 | [8](2025_descriptions_with_tests.md#day-8) | Powering up Christmas decorations                                                                   |
+| [9](2025_descriptions_with_tests.md#day-9) | The input are the coordinates of the red tiles.                                                     |
diff --git a/Advents/AoC2025/2025_descriptions_with_tests.md b/Advents/AoC2025/2025_descriptions_with_tests.md
index 1773372..c48ec26 100644
--- a/Advents/AoC2025/2025_descriptions_with_tests.md
+++ b/Advents/AoC2025/2025_descriptions_with_tests.md
@@ -287,3 +287,36 @@ added.
 [Solution in Lean](day08.lean)
 
 ---
+
+#  [Day 9](https://adventofcode.com/2025/day/9)
+
+The input are the coordinates of the red tiles.
+
+####  Test
+
+<pre>
+7,1
+11,1
+11,7
+9,7
+9,5
+2,5
+2,3
+7,3
+</pre>
+
+### Description
+
+#### Part 1
+
+In part 1, we should determine the largest area of a rectangle with two opposite corners
+on the red tiles.
+
+#### Part 2
+
+In part 2, we should still find the largest rectangle with opposite vertices on the red tiles,
+but the rectangle must be entirely contained in the interior of the path.
+
+[Solution in Lean](day09.lean)
+
+---
diff --git a/Advents/AoC2025/day09.input b/Advents/AoC2025/day09.input
new file mode 100644
index 0000000..5671bb5
--- /dev/null
+++ b/Advents/AoC2025/day09.input
@@ -0,0 +1,496 @@
+98346,50117
+98346,51321
+97590,51321
+97590,52570
+98378,52570
+98378,53784
+98153,53784
+98153,54933
+97379,54933
+97379,56194
+97715,56194
+97715,57357
+97262,57357
+97262,58502
+96789,58502
+96789,59844
+97322,59844
+97322,60862
+96301,60862
+96301,62158
+96496,62158
+96496,63353
+96245,63353
+96245,64573
+96059,64573
+96059,65697
+95564,65697
+95564,66656
+94642,66656
+94642,68048
+94866,68048
+94866,69061
+94123,69061
+94123,70153
+93582,70153
+93582,71391
+93344,71391
+93344,72190
+92231,72190
+92231,73500
+92100,73500
+92100,74339
+91119,74339
+91119,75394
+90523,75394
+90523,76365
+89795,76365
+89795,77786
+89716,77786
+89716,78751
+88956,78751
+88956,79523
+87950,79523
+87950,80419
+87122,80419
+87122,81374
+86368,81374
+86368,82436
+85727,82436
+85727,83340
+84904,83340
+84904,84297
+84131,84297
+84131,84951
+83062,84951
+83062,85736
+82129,85736
+82129,86195
+80920,86195
+80920,87238
+80214,87238
+80214,87725
+79055,87725
+79055,88764
+78320,88764
+78320,89657
+77460,89657
+77460,89956
+76194,89956
+76194,91070
+75461,91070
+75461,91758
+74445,91758
+74445,92101
+73235,92101
+73235,92261
+71945,92261
+71945,93283
+71101,93283
+71101,93988
+70082,93988
+70082,94522
+68978,94522
+68978,94976
+67839,94976
+67839,95058
+66563,95058
+66563,95021
+65267,95021
+65267,95501
+64155,95501
+64155,96035
+63051,96035
+63051,96082
+61812,96082
+61812,96820
+60745,96820
+60745,97209
+59582,97209
+59582,96899
+58288,96899
+58288,97446
+57151,97446
+57151,97443
+55925,97443
+55925,97781
+54742,97781
+54742,97847
+53527,97847
+53527,97964
+52316,97964
+52316,97780
+51095,97780
+51095,98318
+49883,98318
+49883,97566
+48679,97566
+48679,97545
+47473,97545
+47473,97451
+46270,97451
+46270,98168
+44983,98168
+44983,97283
+43861,97283
+43861,97748
+42566,97748
+42566,97553
+41358,97553
+41358,96726
+40279,96726
+40279,96793
+39022,96793
+39022,96846
+37749,96846
+37749,96565
+36553,96565
+36553,95546
+35588,95546
+35588,95771
+34230,95771
+34230,95439
+33045,95439
+33045,94564
+32073,94564
+32073,94197
+30906,94197
+30906,93871
+29713,93871
+29713,92803
+28875,92803
+28875,92611
+27610,92611
+27610,92347
+26361,92347
+26361,90998
+25731,90998
+25731,90775
+24447,90775
+24447,89904
+23562,89904
+23562,88985
+22725,88985
+22725,88768
+21386,88768
+21386,87803
+20591,87803
+20591,86828
+19821,86828
+19821,86644
+18387,86644
+18387,85516
+17755,85516
+17755,84696
+16858,84696
+16858,84108
+15726,84108
+15726,82980
+15135,82980
+15135,81765
+14668,81765
+14668,80912
+13814,80912
+13814,80362
+12579,80362
+12579,79279
+11983,79279
+11983,78255
+11324,78255
+11324,77249
+10646,77249
+10646,76260
+9943,76260
+9943,75253
+9265,75253
+9265,74137
+8769,74137
+8769,73091
+8159,73091
+8159,72007
+7619,72007
+7619,70921
+7086,70921
+7086,69804
+6620,69804
+6620,68965
+5508,68965
+5508,67845
+5008,67845
+5008,66451
+5247,66451
+5247,65435
+4483,65435
+4483,64370
+3807,64370
+3807,62988
+4187,62988
+4187,61973
+3289,61973
+3289,60792
+2976,60792
+2976,59480
+3292,59480
+3292,58342
+2797,58342
+2797,57109
+2829,57109
+2829,55995
+1994,55995
+1994,54760
+2034,54760
+2034,53543
+1929,53543
+1929,52296
+2446,52296
+2446,51110
+1556,51110
+1556,50108
+94697,50108
+94697,48668
+2048,48668
+2048,47447
+1975,47447
+1975,46221
+1919,46221
+1919,45042
+2390,45042
+2390,43799
+2240,43799
+2240,42668
+2906,42668
+2906,41385
+2599,41385
+2599,40229
+3033,40229
+3033,39000
+3116,39000
+3116,37837
+3488,37837
+3488,36745
+4099,36745
+4099,35590
+4459,35590
+4459,34522
+5075,34522
+5075,33098
+4701,33098
+4701,32139
+5600,32139
+5600,31152
+6372,31152
+6372,30021
+6793,30021
+6793,28669
+6780,28669
+6780,27498
+7176,27498
+7176,26736
+8325,26736
+8325,25614
+8804,25614
+8804,24425
+9189,24425
+9189,23412
+9869,23412
+9869,22361
+10494,22361
+10494,21371
+11210,21371
+11210,20320
+11848,20320
+11848,19835
+13189,19835
+13189,18548
+13542,18548
+13542,18030
+14786,18030
+14786,16513
+14942,16513
+14942,16156
+16320,16156
+16320,15426
+17294,15426
+17294,14589
+18162,14589
+18162,13554
+18865,13554
+18865,12508
+19580,12508
+19580,11712
+20511,11712
+20511,11495
+21868,11495
+21868,10721
+22802,10721
+22802,9580
+23501,9580
+23501,9343
+24795,9343
+24795,8400
+25647,8400
+25647,7597
+26598,7597
+26598,7290
+27821,7290
+27821,6954
+29014,6954
+29014,6287
+30043,6287
+30043,6019
+31252,6019
+31252,5325
+32280,5325
+32280,5104
+33495,5104
+33495,4777
+34664,4777
+34664,4504
+35846,4504
+35846,3826
+36908,3826
+36908,3702
+38132,3702
+38132,3406
+39306,3406
+39306,3383
+40537,3383
+40537,2845
+41666,2845
+41666,2992
+42915,2992
+42915,2459
+44062,2459
+44062,1987
+45234,1987
+45234,2539
+46501,2539
+46501,2138
+47688,2138
+47688,2150
+48903,2150
+48903,1538
+50117,1538
+50117,2006
+51332,2006
+51332,2553
+52521,2553
+52521,2295
+53748,2295
+53748,2232
+54974,2232
+54974,2289
+56193,2289
+56193,2272
+57429,2272
+57429,2341
+58660,2341
+58660,3021
+59772,3021
+59772,3447
+60921,3447
+60921,3629
+62126,3629
+62126,3932
+63302,3932
+63302,4676
+64340,4676
+64340,4457
+65690,4457
+65690,4946
+66809,4946
+66809,5755
+67797,5755
+67797,5513
+69218,5513
+69218,6439
+70142,6439
+70142,7122
+71161,7122
+71161,7836
+72154,7836
+72154,7981
+73455,7981
+73455,8711
+74439,8711
+74439,8936
+75733,8936
+75733,10147
+76403,10147
+76403,10678
+77509,10678
+77509,11358
+78519,11358
+78519,12124
+79464,12124
+79464,12881
+80415,12881
+80415,13723
+81295,13723
+81295,14502
+82227,14502
+82227,15128
+83308,15128
+83308,16376
+83787,16376
+83787,17042
+84839,17042
+84839,17766
+85851,17766
+85851,18843
+86471,18843
+86471,19620
+87442,19620
+87442,20888
+87797,20888
+87797,21624
+88839,21624
+88839,22535
+89663,22535
+89663,23943
+89744,23943
+89744,24843
+90578,24843
+90578,25629
+91630,25629
+91630,26746
+92135,26746
+92135,27723
+92898,27723
+92898,28916
+93246,28916
+93246,30250
+93259,30250
+93259,31171
+94169,31171
+94169,32171
+94949,32171
+94949,33395
+95168,33395
+95168,34439
+95886,34439
+95886,35658
+96099,35658
+96099,36857
+96354,36857
+96354,38119
+96346,38119
+96346,39276
+96726,39276
+96726,40399
+97295,40399
+97295,41680
+97073,41680
+97073,42904
+97079,42904
+97079,44093
+97286,44093
+97286,45275
+97608,45275
+97608,46441
+98277,46441
+98277,47695
+97720,47695
+97720,48909
+97577,48909
+97577,50117
diff --git a/Advents/AoC2025/day09.lean b/Advents/AoC2025/day09.lean
new file mode 100644
index 0000000..1d09d76
--- /dev/null
+++ b/Advents/AoC2025/day09.lean
@@ -0,0 +1,85 @@
+import Advents.Utils
+open Std
+
+/-!
+The input are the coordinates of the red tiles.
+-/
+
+namespace AoC2025_Day09
+
+open System in
+/-- `input` is the location of the file with the data for the problem. -/
+def input : FilePath := ("Advents"/"AoC2025"/"day09" : FilePath).withExtension "input"
+
+/-!
+#  Question 1
+
+In part 1, we should determine the largest area of a rectangle with two opposite corners
+on the red tiles.
+-/
+
+/-- `test` is the test string for the problem. -/
+def test := "7,1
+11,1
+11,7
+9,7
+9,5
+2,5
+2,3
+7,3"
+
+/-
+........3←2
+........↓.↑
+.5←←←←←←4.↑
+.↓........↑
+.6→→→→7...↑
+......↓...↑
+......0→→→1
+-/
+
+
+/-- `atest` is the test string for the problem, split into rows. -/
+def atest := (test.splitOn "\n").toArray
+
+/--
+Converts the input to the `HashSet` of positions of the red tiles.
+-/
+def inputToPos (dat : Array String) : HashSet pos :=
+  dat.foldl (init := ∅) fun tot s => match s.getNats with | [x, y] => tot.insert (x, y) | _ => tot
+
+/-- `part1 dat` takes as input the input of the problem and returns the solution to part 1. -/
+def part1 (dat : Array String) : Nat := Id.run do
+  let gr := inputToPos dat
+  let mut maxArea := 0
+  let mut left := gr
+  for A@(a, b) in gr do
+    left := left.erase A
+    for (c, d) in left do
+      let newArea := ((a - c).natAbs + 1) * ((b - d).natAbs + 1)
+      maxArea := max maxArea newArea
+  return maxArea
+
+
+#assert part1 atest == 50
+
+set_option trace.profiler true in solve 1 4767418746
+
+/-!
+#  Question 2
+
+In part 2, we should still find the largest rectangle with opposite vertices on the red tiles,
+but the rectangle must be entirely contained in the interior of the path.
+-/
+
+#exit
+
+/-- `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_Day09