Advent Of Code 2025 - Day 1

Stream: general

[Alfredo Moreira-Rosa]

Not sure if it's allowed to post advent of code solutions here or if it's against our zulip policy. Tell me.

So here is my solution for Day 1. No proofs, just algorithm. I'm insterrested in participating in formal proofs of some of them, it may be fun.

Solution

import LeanAoc.utils.List

inductive ParseError
  | invalidNumber (direction : Char) (rest : List Char)
  | invalidDirection (c : Char) (s : String)
  | emptyInstruction

instance : ToString ParseError where
  toString
  | .invalidNumber dir rest => s!"Invalid number after '{dir}': '{String.mk rest}'"
  | .invalidDirection c s => s!"Invalid direction '{c}', expected 'L' or 'R' in: '{s}'"
  | .emptyInstruction => "Empty instruction"

def ParseError.toIO (e : ParseError) : IO.Error := .userError (toString e)

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

def parseInstruction (s : String) : Except ParseError Int := do
  match s.toList with
  | 'L' :: rest =>
    match (String.mk rest).toInt? with
    | some n => return (-n)
    | none => throw <| .invalidNumber 'L' rest
  | 'R' :: rest =>
    match (String.mk rest).toInt? with
    | some n => return n
    | none => throw <| .invalidNumber 'R' rest
  | c :: _ => throw <| .invalidDirection c s
  | [] => throw .emptyInstruction

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

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

-- PART 1

def dialOne (point: Int) (instruction: Int) : Int :=
  (point + instruction) % 100

def dialInstructions (list: List Int) (init: Int):=
  list.scanl dialOne init

def secret_part1 (instructions: List Int) : Nat :=
  let dialed := dialInstructions instructions 50
  dialed.count 0

#eval do
  let instructions ← parseInput "L68\nL30\nR48\nL5\nR60\nL55\nL1\nL99\nR14\nL82"
  return secret_part1 instructions

#eval do
  let input ← readInput
  let instructions ← parseInput input
  return secret_part1 instructions

-- PART 2

def crossings (x : Int × Int) : Nat :=
  let lo := min x.1 (x.2 - 1)
  let hi := max (x.1 - 1) x.2
  (hi / 100 - lo / 100).toNat

def cumulativePositions (list : List Int) (init: Int) : List Int :=
  (init :: list).scanl (· + ·) 0

def secret_part2 (instructions : List Int) : Nat :=
  let positions := cumulativePositions instructions 50
  positions.pairs.map crossings |>.sum

#eval do
  let instructions ← parseInput "L68\nL30\nR48\nL5\nR60\nL55\nL1\nL99\nR14\nL82"
  return secret_part2 instructions

#eval do
  let input ← readInput
  let instructions ← parseInput input
  return secret_part2 instructions

[Kim Morrison]

I have Claude working on AoC in Lean at https://github.com/kim-em/AoC2025. I set up the repository initially (based on https://www.anthropic.com/engineering/effective-harnesses-for-long-running-agents), without looking at any problems. The first 3 days of problems were successfully completed (including submission) by: claude -p 'Work on AoC'. It took ~10 minutes.

(No proofs here, just programming.)

[Alfredo Moreira-Rosa]

The parsing code part of Claude has some flows. It assumes input data is well formed. It's usually true, but if we want to derive a proof on top of the solution, it will give bad results.
Maybe add some instructions to tell it to handle all parsing edge cases.
I think parsing is one of the most important part of AOC, because it can have the most impact on proper modeling of the problem.

[Kim Morrison]

I don't think it would be cheating to observe what it did on Days 1-3, and then adjust the prompting and throw out its progress and start over. I had initially intended to ask it to write proofs, but did want to put any significant time into this. If someone wants to fork that repo and write prompts that ask for robust code, and specs, and proofs, that would be fun. :-)

[Chris Henson]

For parsing AoC I like to use docs#Std.Internal.Parsec. I think it makes things a lot simpler and more readable.

[Markus Himmel]

Consider using https://github.com/fgdorais/lean4-parser instead. I hear it has more features and it's better supported

[Alfredo Moreira-Rosa]

Thank you Markus, i'll try it.

[Joseph]

https://github.com/josephmate/AdventOfCode2025/blob/main/AdventOfCode2025/Day01.lean

I regret not solving click by click. It resulted in a lot of edge cases to figure it which left me missing a debugger.

[Yaël Dillies]

Here's my solution for AoC day 1, without the parsing part, and formally verified (very easy thanks to grind :heart_eyes:):

import Batteries.Data.List.Basic

def aoc1 (l : List Int) : Nat := (loop l).1
  where loop : List Int → Nat × Nat
  | [] => (0, 50)
  | a :: l =>
    let (count, sum) := loop l
    let newsum := ((a + sum) % 100).toNat
    if newsum == 0 then
      (count + 1, 0)
    else
      (count, newsum)

theorem aoc1Loop_correct :
    ∀ l : List Int, aoc1.loop l = (l.tails.countP (100 ∣ 50 + ·.sum), ((l.sum + 50) % 100).toNat)
  | [] => by simp [aoc1.loop]
  | a :: l => by simp [aoc1.loop, aoc1Loop_correct]; grind

theorem aoc1_correct (l : List Int) : aoc1 l = l.tails.countP (100 ∣ 50 + ·.sum) := by
  simp [aoc1, aoc1Loop_correct]

[Eric Rodriguez]

I'm not sure if this is PEBKAC, but I'm finding it quite hard to get decent compile times. On mathlib@v4.27.0-rc1, this file takes 10s every time I run lake build:

import Parser -- fgdorais one
import Std
import Mathlib.Data.ZMod.Basic

If I import all of Mathlib it's more like 51 seconds. When I get it going / on VSCode after it loads, it's fine, but it's kind of surprising it takes that long to me. It seems to be mostly Mathlib. Is this a side-effect of the module system for non-modules? I can't use a module here sadly as Parser hasn't been updated...

[Eric Rodriguez]

hmm, I actually can't repro anymore after some fiddling, now it remains OK after lake building enough after editing a file. But I do swear it was very slow before starting to type this up... alas ^^

[Kevin Buzzard]

When I had repeated lake builds taking a long time it was my antivirus. The n+1st build would be quick if it was straight after the n'th build but slow if I waited for a few minutes.

[Eric Rodriguez]

Hmm, I'm on a mac so I didn't consider this but I do know that apple now has a default antivirus too

[Shreyas Srinivas]

Are you sure it's not something your institution installed?

[Shreyas Srinivas]

In Kevin's case, I think it was Sophos

[Eric Rodriguez]

this is my personal laptop haha

[Kevin Buzzard]

(I'm on a mac and it was Microsoft Defender)