diff --git a/AoC2024Lean/AoC2024d07p1.lean b/AoC2024Lean/AoC2024d07p1.lean
new file mode 100644
index 0000000..c5ef44e
--- /dev/null
+++ b/AoC2024Lean/AoC2024d07p1.lean
@@ -0,0 +1,38 @@
+import AoC2024Lean.LittleHelpers
+
+open Std.Internal Parsec Lean.Parser
+open Std.Internal.Parsec.String
+
+structure Calibration where
+  value : Nat
+  numbers : List Nat
+
+partial def Calibration.valid (clbr : Calibration) : Nat :=
+  match clbr.numbers with
+  | [] => 0
+  | n₁ :: ns => match ns with
+    | [] => if (n₁ == clbr.value) then 1 else 0
+    | n₂ :: ns' =>
+      let withAdd : Calibration := {value := clbr.value, numbers := (n₁ + n₂) :: ns'}
+      let withMul : Calibration := {value := clbr.value, numbers := (n₁ * n₂) :: ns'}
+      withAdd.valid + withMul.valid
+
+def totalCalibration (calibs : List Calibration) : Nat :=
+  List.sum <| calibs.map fun c ↦ if c.valid > 0 then c.value else 0
+
+def parseCalibration : Parser Calibration := do
+  let val ← digits
+  _ ← pstring ": "
+  let ns ← digits.separated (pchar ' ')
+  return {value := val, numbers := ns}
+
+def parseInput : Parser (List Calibration) := do
+  let cs ← many ((attempt $ parseCalibration) <* (many $ pchar '\n'))
+  return cs.toList
+
+def main : IO Unit := do
+  let input ← (IO.FS.readFile "./AoC2024Lean/input-AoC2024d07p1.txt")
+  let calibs := optList (parseInput.run input).toOption
+  IO.println <| s!"Total calibration : {totalCalibration calibs}"
+
+--#eval main -- Total calibration : 3749
diff --git a/AoC2024Lean/AoC2024d07p2.lean b/AoC2024Lean/AoC2024d07p2.lean
new file mode 100644
index 0000000..feb34f3
--- /dev/null
+++ b/AoC2024Lean/AoC2024d07p2.lean
@@ -0,0 +1,42 @@
+import AoC2024Lean.LittleHelpers
+
+open Std.Internal Parsec Lean.Parser
+open Std.Internal.Parsec.String
+
+structure Calibration where
+  value : Nat
+  numbers : List Nat
+
+def concatNum (a b : Nat) : Nat :=
+  optNum <| (toString a ++ toString b).toNat?
+
+partial def Calibration.valid (clbr : Calibration) : Nat :=
+  match clbr.numbers with
+  | [] => 0
+  | n₁ :: ns => match ns with
+    | [] => if (n₁ == clbr.value) then 1 else 0
+    | n₂ :: ns' =>
+      let withAdd : Calibration := {value := clbr.value, numbers := (n₁ + n₂) :: ns'}
+      let withMul : Calibration := {value := clbr.value, numbers := (n₁ * n₂) :: ns'}
+      let withCat : Calibration := {value := clbr.value, numbers := (concatNum n₁ n₂) :: ns'}
+      withAdd.valid + withMul.valid + withCat.valid
+
+def totalCalibration (calibs : List Calibration) : Nat :=
+  List.sum <| calibs.map fun c ↦ if c.valid > 0 then c.value else 0
+
+def parseCalibration : Parser Calibration := do
+  let val ← digits
+  _ ← pstring ": "
+  let ns ← digits.separated (pchar ' ')
+  return {value := val, numbers := ns}
+
+def parseInput : Parser (List Calibration) := do
+  let cs ← many ((attempt $ parseCalibration) <* (many $ pchar '\n'))
+  return cs.toList
+
+def main : IO Unit := do
+  let input ← (IO.FS.readFile "./AoC2024Lean/input-AoC2024d07p1.txt")
+  let calibs := optList (parseInput.run input).toOption
+  IO.println <| s!"Total calibration : {totalCalibration calibs}"
+
+--#eval main -- Total calibration : 11387
diff --git a/AoC2024Lean/LittleHelpers.lean b/AoC2024Lean/LittleHelpers.lean
index 38b6c00..fc0d34b 100644
--- a/AoC2024Lean/LittleHelpers.lean
+++ b/AoC2024Lean/LittleHelpers.lean
@@ -187,6 +187,10 @@ def String.removeAny (orig : String) (rems : List String) : String :=
     | r :: rs, s => helper rs (s.remove r)
   helper rems orig
 
+def Std.Internal.Parsec.String.Parser.separated {α β : Type} (p : Parser β) (sep : Parser α) :
+    Parser (List β) := do
+  return (← p) :: (← many (sep *> p)).toList
+
 end String_helpers -- section
 
 
diff --git a/AoC2024Lean/input-AoC2024d07p1.txt b/AoC2024Lean/input-AoC2024d07p1.txt
new file mode 100644
index 0000000..87b8b25
--- /dev/null
+++ b/AoC2024Lean/input-AoC2024d07p1.txt
@@ -0,0 +1,9 @@
+190: 10 19
+3267: 81 40 27
+83: 17 5
+156: 15 6
+7290: 6 8 6 15
+161011: 16 10 13
+192: 17 8 14
+21037: 9 7 18 13
+292: 11 6 16 20
\ No newline at end of file