Advent Of Code 2025 - Day 3

Stream: general

[Alfredo Moreira-Rosa]

Here is my solution for Day 3.
I was lucky to make the algorithm generic since the beginning so it worked with the same code for part 2.

Solution

import LeanAoc.utils.List

inductive ParseError
  | invalidCharacter (c : Char) (line : String)
  | emptyBank
  | tooFewDigits (count : Nat) (expected : Nat)

instance : ToString ParseError where
  toString
  | .invalidCharacter c line => s!"Invalid character '{c}' in line: '{line}'"
  | .emptyBank => "Empty battery bank"
  | .tooFewDigits count expected => s!"Battery bank has only {count} digit(s), need at least {expected}"

instance : Coe ParseError IO.Error where
  coe e := IO.userError (toString e)

instance : MonadLift (Except ParseError) IO where
  monadLift
  | .ok a => return a
  | .error e => throw ↑e

def parseLine (s : String) (minDigits: Nat) : Except ParseError (List Nat) := do
  if s.isEmpty then
    throw .emptyBank
  for c in s.toList do
    if !c.isDigit then
      throw <| .invalidCharacter c s
  let digits := s.toList.map fun c => c.toNat - '0'.toNat
  if digits.length < minDigits then
    throw <| .tooFewDigits digits.length minDigits
  return digits


def parseInput (input : String) (minDigits: Nat) : IO (List (List Nat)) := do
  let lines := input.splitOn "\n"
  List.range lines.length
    |>.zip lines
    |>.mapM fun (lineNum, line) => do
      try
        parseLine line minDigits
      catch e =>
        throw <| IO.userError s!"Line {lineNum + 1}: {e}"

def readInput : IO String := do
  IO.FS.readFile "LeanAoc/day03/input.txt"

-- COMMON

def maxJoltage (digits : List Nat) (k : Nat) : Nat :=
  let n := digits.length
  if k = 0 ∨ k > n then 0
  else
    let (_, _, result) := List.range k
      |>.foldl (init := (digits, n, 0)) fun (remaining, remLen, acc) i =>
        let windowSize := remLen - (k - i - 1)
        let (bestDigit, bestIdx) := remaining.maxWithIndex windowSize
        (remaining.drop (bestIdx + 1), remLen - bestIdx - 1, acc * 10 + bestDigit)
    result

def totalJoltage (banks : List (List Nat)) (k: Nat) : Nat :=
  banks.map (maxJoltage · k) |>.sum

-- PART 1

/--
info: 357
-/
#guard_msgs in
#eval do
  let input := "987654321111111\n811111111111119\n234234234234278\n818181911112111"
  let banks ← parseInput input 2
  return totalJoltage banks 2

#guard_msgs in
#eval do
  let input ← readInput
  let banks ← parseInput input 2
  return totalJoltage banks 2

-- PART 2

/--
info: 3121910778619
-/
#guard_msgs in
#eval do
  let input := "987654321111111\n811111111111119\n234234234234278\n818181911112111"
  let banks ← parseInput input 12
  return totalJoltage banks 12

#eval do
  let input ← readInput
  let banks ← parseInput input 12
  return totalJoltage banks 12

with the following code for minWithIndex :

def maxWithIndex [Zero α] [LT α] [DecidableRel (α := α) (· < ·)] (l : List α) (size : Nat) : (α × Nat) :=
  go l 0 0 0 size
where
  go (xs : List α) (idx : Nat) (maxVal : α) (maxIdx : Nat) (remaining : Nat) : (α × Nat) :=
    if remaining = 0 then
      (maxVal, maxIdx)
    else
      match xs with
      | [] => (maxVal, maxIdx)
      | x :: rest =>
        if maxVal < x then
          go rest (idx + 1) x idx (remaining - 1)
        else
          go rest (idx + 1) maxVal maxIdx (remaining - 1)

[Alfredo Moreira-Rosa]

The time complexity of the algorithm is $O(n.m)$ where n is the max number of batteries to combine and m is the number of banks.

[Jason Orendorff]

https://github.com/jorendorff/advent-of-code/blob/main/2025/day03/Day03/Basic.lean

Solution

import Std.Internal.Parsec

open Std.Internal.Parsec
open Std.Internal.Parsec.String
-- # Input parser

abbrev Input := Array (Array Nat)

def battery : Parser Nat := do
  let d <- digit
  return d.toNat - '0'.toNat

def bank : Parser (Array Nat) := do
  let chars <- many battery
  skipChar '\n'
  return chars

def parser : Parser Input := many bank
-- # Part 1

def bankJoltage1 (bank : Array Nat) : Nat :=
  let acc := fun (state : Nat × Nat) (bat : Nat) =>
    let ⟨pairMax, batMax⟩ := state
    (max pairMax (10 * batMax + bat), max batMax bat)
  let ⟨pairMax, _⟩ := bank.foldl acc ⟨0, 0⟩
  pairMax

def solve1 (input : Input) : Nat :=
  input.map bankJoltage1 |>.sum
-- # Part 2

def enumerate {α : Type} (arr : Array α) : Array (Nat × α) :=
  Array.range arr.size |>.zip arr

def handleDigit (len : Nat) (k : Nat) (acc : Array Nat) (item : Nat × Nat) : Array Nat :=
  let ⟨i, digit⟩ := item
  if _ : i + k < acc.size + len ∧ acc.size > 0 ∧ acc.back! < digit
  then handleDigit len k acc.pop item
  else if acc.size < k
    then acc.push digit
    else acc
termination_by acc.size

def bankJoltage2 (bank : Array Nat) : Nat :=
  enumerate bank
    |>.foldl (handleDigit bank.size 12) #[]
    |>.foldl (fun acc digit => 10 * acc + digit) 0

def solve2 (input : Input) : Nat :=
  input.map bankJoltage2 |>.sum

[Alfredo Moreira-Rosa]

Just in case you didn't know, there is native enumerate in lean : docs#List.zipIdx and docs#Array.zipIdx