Advent Of Code 2025 - Day 6

Stream: general

[Alfredo Moreira-Rosa]

Here is my solution for Day 6 of advent of code. This time the interresting logic is coming from the parser.
For the first problem we needed to transpose at the Word level, while for the second it's at the Character level.
Appart from that it's just simple operations.

Solution

import LeanAoc.utils.List

namespace Day06

-- MODELS

inductive Operator
  | add
  | mul
deriving Inhabited, Repr, DecidableEq

structure Operation where
  operator : Operator
  numbers  : List Nat
deriving Inhabited, Repr, DecidableEq
-- PARSER

inductive ParserError
  | invalidNumber (n : String)
  | invalidOperator (s : String)
  | missingOperators
  | emptyInput

instance : ToString ParserError where
  toString
  | .invalidNumber n => s!"Invalid number: '{n}'"
  | .invalidOperator s => s!"Invalid operator, expected '+' or '*' but got: '{s}'"
  | .missingOperators => "Missing operators line"
  | .emptyInput => "Empty input"

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

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

def parseNumber (s : String) : Except ParserError Nat :=
  match s.toNat? with
  | some n => return n
  | none => throw <| .invalidNumber s

def parseOperator (s : String) : Except ParserError Operator :=
  match s with
  | "+" => return Operator.add
  | "*" => return Operator.mul
  | _   => throw <| .invalidOperator s

def words (s : String) : List String :=
  s.splitOn " " |>.filter (· ≠ "")

def parseOperation (words : List String) : Except ParserError Operation := do
  match words.splitAt (words.length - 1) with
  | (numStr, [opStr]) => do
    let numbers ← numStr.mapM parseNumber
    let op ← parseOperator opStr
    return ⟨op, numbers⟩
  | _ => throw <| .missingOperators

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

-- PART 1

def parseInputPart1 (input : String) : Except ParserError (List Operation) :=
  input.splitOn "\n"
    |>.map words
    |>.transpose
    |>.mapM parseOperation

def solveOperation (operation: Operation) : Nat :=
  match operation.operator with
  | .add => operation.numbers.sum
  | .mul => operation.numbers.prod

def grandTotal (operations: List Operation) : Nat :=
  operations.map solveOperation |>.sum

/--
info: 4277556
-/
#guard_msgs in
#eval do
  let input := "123 328  51 64 \n 45 64  387 23 \n  6 98  215 314\n*   +   *   +  "
  let operations ← parseInputPart1 input
  return grandTotal operations

#eval do
  let input := ← readInput
  let operations ← parseInputPart1 input
  return grandTotal operations

-- PART 2

def splitOp (s: String) : List String :=
  match s.toList.getLast?  with
  | some '+' => ["+", s.dropRight 1]
  | some '*' => ["*", s.dropRight 1]
  | _ => [s]

def isNotBlank (s : String) : Bool :=
  s.trim ≠ ""

def atOperator (_ s : String) : Bool :=
  s ≠ "+" && s ≠ "*"

def parseInputPart2 (input : String) : Except ParserError (List Operation) :=
  input.splitOn "\n"
    |>.map String.toList
    |>.transpose
    |>.map String.mk
    |>.flatMap splitOp
    |>.map String.trim
    |>.filter isNotBlank
    |>.splitBy atOperator
    |>.map List.reverse
    |>.mapM parseOperation

/--
info: 3263827
-/
#guard_msgs in
#eval do
  let input := "123 328  51 64 \n 45 64  387 23 \n  6 98  215 314\n*   +   *   +  "
  let operations ← parseInputPart2 input
  return grandTotal operations

#eval do
  let input := ← readInput
  let operations ← parseInputPart2 input
  return grandTotal operations

end Day06

[Rado Kirov]

With Claude's help I translated some of my TS solutions for day 1,2,3

What's most interesting to me is adding some theorems (since I don't need one more FP language, but FP language with proofs is truly novel). I wrote some statements that could be of interest, but couldn't even begin proving them:

• day 3
• day 2
• day 1

[Kim Morrison]

My Claude pipeline has continued to succeed at Advent of Code in Lean.

Since starting, all I have done is repeatedly run claude -p 'Please work on AoC.'.

(EDIT: oh, that's not quite true: after Markus's reminder to use fgdorais/lean4-parser, after Day 1 I updated the prompting to suggest that. I also, after Day 3, updated the prompting to tell it that if was all caught up on submitting solutions, it should try to write verification statements and prove them/send them to Aristotle. I haven't actually looked yet at what it has produced in this direction!)

So far, it has solved all problems except Day 9 Part 2 in a matter of minutes. Day 9 Part 2 required three separate invocations of claude -p 'Please work on AoC.', and several hours. But still no human intervention (I only looked at the problem statement after it was successfully submitted).

[Rado Kirov]

Wow, this is amazing. Interesting that while it has no problem writing the code, so many of the proofs are sorries.

[Kim Morrison]

Note that asking it to write proofs was an afterthought, with zero effort into getting useful prompting, and I haven't even looked at the output proofs yet! I wouldn't read too much into its performance here.

[Kim Morrison]

(Claude just solved Day 11, in just a few minutes. Only one day to go!)

[Rado Kirov]

impressive given that lean programs don't have a large training corpus, it must mean that it can fairly easily translate between languages. I am doing the problems as they come out and averaging around ~20min per problem (I have copilot on, but otherwise try not to use AI).

The last day usually is relatively easy and there is only part1, part2 is just unlocking the final screen if you have solved all the other problems.

[Alfredo Moreira-Rosa]

It's nice to know that Claude can do it all by itself, but for me using AI kills the fun out of it :sweat_smile:

[Kim Morrison]

Oh, of course, chess is still fun too. But it's good to keep track of what the current capabilities are, so when it's not fun you know which tools are relevant!