Advent Of Code 2025 - Day 2

Stream: general

[Alfredo Moreira-Rosa]

Here is my solution for Day 2 of advent of code.
Solution is straigth forward, for each range, compute the possible repeating patterns, then sum them up :

Solution

inductive ParseError
  | invalidNumber (a b : String)
  | invalidRangeOrd (l h : Nat)
  | invalidRangeFormat (s : String)

instance : ToString ParseError where
  toString
  | .invalidNumber a b => s!"Invalid number in range: '{a}-{b}'"
  | .invalidRangeOrd l h => s!"Invalid range order: '{l}-{h}', expected lower ≤ higher"
  | .invalidRangeFormat s => s!"Invalid range format: '{s}', expected '<nat>-<nat>'"

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

abbrev Range := Nat × Nat

def parseRange (s : String) : Except ParseError Range := do
  let parts := s.splitOn "-"
  match parts with
  | [a, b] =>
    match (a.toNat?, b.toNat?) with
    | (some na, some nb) =>
      if na ≤ nb then
        return (na, nb)
      else
        throw <| .invalidRangeOrd na nb
    | _ => throw <| .invalidNumber a b
  | _ => throw <| .invalidRangeFormat s

def parseRanges (input : String) : Except ParseError (List Range) :=
  input.splitOn ","
    |>.mapM parseRange

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

-- COMMON

def numDigits (n : Nat) : Nat :=
  if n < 10 then 1
  else 1 + numDigits (n / 10)

def ceilingDiv (a b : Nat) : Nat :=
  (a + b - 1) / b

def invalidIdsWithMultiplier (range : Range) (multiplier : Nat) (d : Nat) : List Nat :=
  let lo := max (ceilingDiv range.1 multiplier) (10 ^ (d - 1))
  let hi := min (range.2 / multiplier) (10 ^ d - 1)
  if lo > hi then []
  else List.range' lo (hi - lo + 1) |>.map (· * multiplier)

-- PART 1

def invalidIdsForDigits (range: Range) (nDigits : Nat) : List Nat :=
  let multiplier := 10 ^ nDigits + 1
  invalidIdsWithMultiplier range multiplier nDigits

def invalidIds (range : Range) : List Nat :=
  let minDigits := (numDigits range.1 + 1) / 2
  let maxDigits := (numDigits range.2 + 1) / 2
  List.range' minDigits (maxDigits - minDigits + 1)
    |>.flatMap (invalidIdsForDigits range)

def sumInvalidIds (ranges : List Range) : Nat :=
  ranges.flatMap invalidIds |>.sum

/--
info: 1227775554
-/
#guard_msgs in
#eval do
  let ranges ← parseRanges "11-22,95-115,998-1012,1188511880-1188511890,222220-222224,1698522-1698528,446443-446449,38593856-38593862,565653-565659,824824821-824824827,2121212118-2121212124"
  return sumInvalidIds ranges

#eval do
  let input ← readInput
  let ranges ← parseRanges input
  return sumInvalidIds ranges
-- PART 2

def computeRepMultiplier (d k : Nat) : Nat :=
  (10 ^ (d * k) - 1) / (10 ^ d - 1)

def invalidIdsForDigitsAndReps (range : Range) (d k : Nat) : List Nat :=
  let multiplier := computeRepMultiplier d k
  invalidIdsWithMultiplier range multiplier d

def invalidRepIds (range : Range) : List Nat :=
  let maxDigits := numDigits range.2 -1
  let pairs := List.range' 1 maxDigits
      |>.flatMap fun d =>
        List.range' 2 (maxDigits / d)
          |>.map (fun k => (d, k))
  pairs.flatMap (fun (d, k) => invalidIdsForDigitsAndReps range d k)
  |>.eraseDups

def sumInvalidRepIds (ranges : List Range) : Nat :=
  ranges.flatMap invalidRepIds |>.sum

/--
info: 4174379265
-/
#guard_msgs in
#eval do
  let ranges ← parseRanges "11-22,95-115,998-1012,1188511880-1188511890,222220-222224,1698522-1698528,446443-446449,38593856-38593862,565653-565659,824824821-824824827,2121212118-2121212124"
  return sumInvalidRepIds ranges

#eval do
  let input ← readInput
  let ranges ← parseRanges input
  return sumInvalidRepIds ranges

[Alfredo Moreira-Rosa]

This solution is not brute forcing (detecting patterns), but does the opposite.
It generates the possible repeating patterns for a range. Hence the use of the numDigits (equivalent of $\log_{10} n$).
Meaning it's complexity is :

• part 1 : $O(\sqrt N*(\log N))$
• part 2 : $O(N * (\log N)^2)$ due to dedup, could be improved using HashSet.