diff --git a/Aoc2024/Day01.lean b/Aoc2024/Day01.lean
deleted file mode 100644
index 07bc503..0000000
--- a/Aoc2024/Day01.lean
+++ /dev/null
@@ -1,48 +0,0 @@
-namespace Aoc2024.Day01
-
-def splitOnWhitespace (s : String) : List String :=
-  s.split Char.isWhitespace |> .filter (· ≠ "")
-
-def getOrExcept (message : String) (o : Option α) : Except String α :=
-  match o with
-  | some x => pure x
-  | none => throw message
-
-def parseNumber (s: String) : Except String Int :=
-  s.toInt? |> getOrExcept s!"Failed to parse as number: {s}"
-
-def getTwoElements (l : List α) : Except String (α × α) := do
-  let [a, b] := l | throw s!"Expected two elements, but got {l.length}"
-  pure (a, b)
-
-def parseTwoNumbers (line : String) : Except String (Int × Int) := do
-  let (a, b) ← getTwoElements (splitOnWhitespace line)
-  Prod.mk <$> parseNumber a <*> parseNumber b
-
-def parseLines (s : String) : Except String (List (Int × Int)) :=
-  s.splitOn "\n" |>.mapM parseTwoNumbers
-
-def sumList (nums : List Int) : Int :=
-  nums.foldl (fun acc x => acc + x) 0
-
-def sumListBy (f : Int → Int) (nums : List Int) : Int :=
-  nums.foldl (fun acc x => acc + f x) 0
-
-theorem testSumListEmpty : sumList [] = 0 := rfl
-theorem testSumList : sumList [1, 2, 3] = 6 := rfl
-
-def solvePart1 (pairs : List (Int × Int)) : Int :=
-  let (firsts, seconds) := pairs.unzip
-  let distance (a b : Int) : Int := (a - b).natAbs
-  (firsts.mergeSort.zipWith distance seconds.mergeSort) |> sumList
-
-def parseAndSolvePart1 (s : String) : Except String Int :=
-  s |> parseLines |> .map solvePart1
-
-def solvePart2 (pairs : List (Int × Int)) : Int :=
-  let (firsts, seconds) := pairs.unzip
-  let similarityScore (n : Int) : Int := seconds.count n * n
-  firsts |> sumListBy similarityScore
-
-def parseAndSolvePart2 (s : String) : Except String Int :=
-  s |> parseLines |>.map solvePart2
diff --git a/Aoc2024/Day01/Parser.lean b/Aoc2024/Day01/Parser.lean
new file mode 100644
index 0000000..88e25b1
--- /dev/null
+++ b/Aoc2024/Day01/Parser.lean
@@ -0,0 +1,18 @@
+import Aoc2024.Utils
+
+def splitOnWhitespace (s : String) : List String :=
+  s.split Char.isWhitespace |> .filter (· ≠ "")
+
+def parseNumber (s: String) : Except String Int :=
+  s.toInt? |> getOrExcept s!"Failed to parse as number: {s}"
+
+def getTwoElements (l : List α) : Except String (α × α) := do
+  let [a, b] := l | throw s!"Expected two elements, but got {l.length}"
+  pure (a, b)
+
+def parseTwoNumbers (line : String) : Except String (Int × Int) := do
+  let (a, b) ← getTwoElements (splitOnWhitespace line)
+  Prod.mk <$> parseNumber a <*> parseNumber b
+
+def parseLines (s : String) : Except String (List (Int × Int)) :=
+  s.splitOn "\n" |>.mapM parseTwoNumbers
diff --git a/Aoc2024/Day01/Solve.lean b/Aoc2024/Day01/Solve.lean
new file mode 100644
index 0000000..20fb009
--- /dev/null
+++ b/Aoc2024/Day01/Solve.lean
@@ -0,0 +1,16 @@
+import Aoc2024.Day01.Parser
+namespace Aoc2024.Day01
+
+def solvePart1 (pairs : List (Int × Int)) : Int :=
+  let (firsts, seconds) := pairs.unzip
+  let distance (a b : Int) : Int := (a - b).natAbs
+  (firsts.mergeSort.zipWith distance seconds.mergeSort) |> sumList
+
+def parseAndSolvePart1 : String -> Except String Int := .map solvePart1 ∘ parseLines
+
+def solvePart2 (pairs : List (Int × Int)) : Int :=
+  let (firsts, seconds) := pairs.unzip
+  let similarityScore (n : Int) : Int := seconds.count n * n
+  firsts |> sumListBy similarityScore
+
+def parseAndSolvePart2 : String -> Except String Int := .map solvePart2 ∘ parseLines
diff --git a/Aoc2024/Utils.lean b/Aoc2024/Utils.lean
new file mode 100644
index 0000000..c2c3019
--- /dev/null
+++ b/Aoc2024/Utils.lean
@@ -0,0 +1,13 @@
+def sumList (nums : List Int) : Int :=
+  nums.foldl (fun acc x => acc + x) 0
+
+theorem testSumListEmpty : sumList [] = 0 := rfl
+theorem testSumList : sumList [1, 2, 3] = 6 := rfl
+
+def sumListBy (f : Int → Int) (nums : List Int) : Int :=
+  nums.foldl (fun acc x => acc + f x) 0
+
+def getOrExcept (message : String) (o : Option α) : Except String α :=
+  match o with
+  | some x => pure x
+  | none => throw message
diff --git a/Main.lean b/Main.lean
index 1e15bbe..bdb1016 100644
--- a/Main.lean
+++ b/Main.lean
@@ -1,22 +1,21 @@
-import Aoc2024.Day01
+import Aoc2024.Day01.Solve
 import Aoc2024.CustomMonadLift
+open Aoc2024.Day01
+
+def solve (name: String) (inputPath: String) : IO Unit := do
+  IO.println name
+  let input <- IO.FS.readFile inputPath
+  let part1 <- parseAndSolvePart1 input
+  IO.println s!"Part 1: {part1}"
+  let part2 <- parseAndSolvePart2 input
+  IO.println s!"Part 2: {part2}"
 
 def main : IO Unit := do
   try
     IO.println "Day 01"
     IO.println ""
-    IO.println "Example input"
-    let exampleInput <- IO.FS.readFile "inputs/day01/example.txt"
-    let examplePart1 <- Aoc2024.Day01.parseAndSolvePart1 exampleInput
-    IO.println s!"Part 1: {examplePart1}"
-    let examplePart2 <- Aoc2024.Day01.parseAndSolvePart2 exampleInput
-    IO.println s!"Part 2: {examplePart2}"
+    solve "Example" "inputs/day01/example.txt"
     IO.println ""
-    IO.println "Puzzle input"
-    let puzzleInput ← IO.FS.readFile "inputs/day01/input.txt"
-    let part1 <- Aoc2024.Day01.parseAndSolvePart1 puzzleInput
-    IO.println s!"Part 1: {part1}" -- 2066446
-    let part2 <- Aoc2024.Day01.parseAndSolvePart2 puzzleInput
-    IO.println s!"Part 2: {part2}" -- 24931009
+    solve "Puzzle" "inputs/day01/input.txt" -- 2066446, 24931009
   catch e =>
     IO.println s!"Caught exception: {e}"
diff --git a/README.md b/README.md
index 359c390..ead18b3 100644
--- a/README.md
+++ b/README.md
@@ -1,3 +1,5 @@
-# Day 1
+https://github.com/chenson2018/advent-of-code/blob/main/2024/lean/AoC/Day01.lean
+https://github.com/kiranandcode/lean-aoc/blob/main/Solutions/Day1.lean
+
 How to do unit tests / basic theorems for particular values?
-How can I build different executables in Lakefile for each day?
+Build different executables in Lakefile for each day?