I wrote today’s program in Python. (I am going to do a different language each day.) The only thing that gave me a little trouble was I was counting “\n” as a part label. Once I realized that I was able to get both problems done very quickly.

My code for the two parts is on github:-

• https://github.com/pngwen/advent-2023/blob/main/day-3a.py
• https://github.com/pngwen/advent-2023/blob/main/day-3b.py

Python

Questions and comments welcome!

import collections
import re

from .solver import Solver

class Day03(Solver):
  def __init__(self):
    super().__init__(3)
    self.lines = []

  def presolve(self, input: str):
    self.lines = input.rstrip().split('\n')

  def solve_first_star(self):
    adjacent_to_symbols = set()
    for i, line in enumerate(self.lines):
      for j, sym in enumerate(line):
        if sym in ('0', '1', '2', '3', '4', '5', '6', '7', '8', '9', '.'):
          continue
        for di in (-1, 0, 1):
          for dj in (-1, 0, 1):
            adjacent_to_symbols.add((i + di, j + dj))
    numbers = []
    for i, line in enumerate(self. lines):
      for number_match in re.finditer(r'\d+', line):
        is_adjacent_to_symbol = False
        for j in range(number_match.start(), number_match.end()):
          if (i, j) in adjacent_to_symbols:
            is_adjacent_to_symbol = True
        if is_adjacent_to_symbol:
          numbers.append(int(number_match.group()))
    return sum(numbers)

  def solve_second_star(self):
    gear_numbers = collections.defaultdict(list)
    adjacent_to_gears = {}
    for i, line in enumerate(self.lines):
      for j, sym in enumerate(line):
        if sym == '*':
          for di in (-1, 0, 1):
            for dj in (-1, 0, 1):
              adjacent_to_gears[(i + di, j + dj)] = (i, j)
    for i, line in enumerate(self. lines):
      for number_match in re.finditer(r'\d+', line):
        adjacent_to_gear = None
        for j in range(number_match.start(), number_match.end()):
          if (i, j) in adjacent_to_gears:
            adjacent_to_gear = adjacent_to_gears[(i, j)]
        if adjacent_to_gear:
          gear_numbers[adjacent_to_gear].append(int(number_match.group()))
    ratios = []
    for gear_numbers in gear_numbers.values():
      match gear_numbers:
        case [a, b]:
          ratios.append(a * b)
    return sum(ratios)

Rust

I’ve been using Regexes for every day so far, this time it helped in finding numbers along with their start and end position in a line. For the second part I mostly went with the approach of part 1 which was to look at all numbers and then figure out if it has a part symbol around it. Only in part 2 I saved all numbers next to a gear * in a hash table that maps each gear position to a list of adjacent numbers. Then in the end I can just look at all gears with exactly 2 numbers attached.

Also it has to be said, multiplying two numbers is the exact opposite of getting their ratio!

My Python solution for part 1 and part 2. I really practice my regex skills.

#!/usr/bin/python3

import re

value_re = '(\d+)'
symbol_re = '[^\d.]'
gear_re = '(\*)'

def main():
    input = list()
    with open("input.txt", 'r') as in_file:
        for line in in_file:
            input.append(line.strip('\n'))
    length = len(input)
    width = len(input[0])
    value_sum = 0
    for idx, line in enumerate(input):
        for match in re.finditer(value_re, line):
            for line_mask in input[max(idx - 1, 0):min(idx + 2, length)]:
                valid_chars = line_mask[max(match.span()[0] - 1, 0):min(match.span()[1] + 1, width)]
                if re.search(symbol_re, valid_chars):
                    value_sum += int(match[0])
                    break
    print(f"Value sum = {value_sum}")

    gear_ratio = 0
    for idx, line in enumerate(input):
        for match in re.finditer(gear_re, line):
            valid_lines = input[max(idx - 1, 0):min(idx + 2, length)]
            min_range = max(match.span()[0] - 1, 0)
            max_range = min(match.span()[1], width)
            num_of_adjacent = 0
            temp_gear_ratio = 1
            for valid_line in valid_lines:
                for match in re.finditer(value_re, valid_line):
                    if match.span()[0] in range(min_range,max_range + 1) or match.span()[1] - 1 in range(min_range,max_range + 1):
                        num_of_adjacent += 1
                        temp_gear_ratio *= int(match[0])
            if num_of_adjacent == 2:
                gear_ratio += temp_gear_ratio
    print(f"Gear ratio = {gear_ratio}")

if __name__ == '__main__':
    main()

That was not fun to solve. Lots of ugly code. This is a less ugly second version. Language: Nim.

day_03.nim

I only have part 1 finished so far, thanks to a single segfault and me procrastinating on downloading Valgrind…

Anyways here it is!

https://git.sr.ht/~aidenisik/aoc23/tree/master/item/day3

C

EDIT: Part 2 is now also uploaded

Factor on github (with comments and imports):

: symbol-indices ( line -- seq )
  [ ".0123456789" member? not ] find-all [ first ] map
;

: num-spans ( line -- seq )
  >array [ over digit? [ nip ] [ 2drop f ] if ] map-index
  { f } split harvest
  [ [ first ] [ last ] bi 2array ] map
;

: adjacent? ( num-span symbol-indices -- ? )
  swap [ first 1 - ] [ last 1 + ] bi [a,b]
  '[ _ interval-contains? ] any?
;

: part-numbers ( line nearby-symbol-indices -- seq )
  [ dup num-spans ] dip
  '[ _ adjacent? ] filter
  swap '[ first2 1 + _ subseq string>number ] map
;

: part1 ( -- )
  "vocab:aoc-2023/day03/input.txt" utf8 file-lines
  [ [ symbol-indices ] map ] keep
  [
    pick swap [ 1 - ?nth-of ] [ nth-of ] [ 1 + ?nth-of ] 2tri
    3append part-numbers sum
  ] map-index sum nip .
;

: star-indices ( line -- seq )
  [ CHAR: * = ] find-all [ first ] map
;

: gears ( line prev-line next-line -- seq-of-pairs )
  pick star-indices
  [ 1array '[ _ part-numbers ] [ 3dup ] dip tri@ 3append ]
  [ length 2 = ] map-filter [ 3drop ] dip
;

: part2 ( -- )
  "vocab:aoc-2023/day03/input.txt" utf8 file-lines
  dup [
    pick swap [ 1 - ?nth-of ] [ 1 + ?nth-of ] 2bi
    gears [ product ] map-sum
  ] map-index sum nip .
;

Language: Python

Classic AoC grid problem… Tedious as usual, but very doable. Took my time and I’m pretty happy with the result. :]

Schematic  = list[str]
Number     = tuple[int, int, int]

DIRECTIONS = (
    (-1, -1),
    (-1,  0),
    (-1,  1),
    ( 0, -1),
    ( 0,  1),
    ( 1, -1),
    ( 1,  0),
    ( 1,  1),
)

def read_schematic(stream=sys.stdin) -> Schematic:
    schematic = [line.strip() for line in stream]
    columns   = len(schematic[0]) + 2
    return [
        '.'*columns,
        *['.' + line + '.' for line in schematic],
        '.'*columns,
    ]

def is_symbol(s: str) -> bool:
    return not (s.isdigit() or s == '.')

def find_numbers(schematic: Schematic) -> Iterator[Number]:
    rows    = len(schematic)
    columns = len(schematic[0])

    for r in range(1, rows):
        for number in re.finditer(r'[0-9]+', schematic[r]):
            yield (r, *number.span())

def find_parts(schematic: Schematic, numbers: Iterator[Number]) -> Iterator[int]:
    for r, c_head, c_tail in numbers:
        part = int(schematic[r][c_head:c_tail])
        for c in range(c_head, c_tail):
            neighbors = (schematic[r + dr][c + dc] for dr, dc in DIRECTIONS)
            if any(is_symbol(neighbor) for neighbor in neighbors):
                yield part
                break

def main(stream=sys.stdin) -> None:
    schematic = read_schematic(stream)
    numbers   = find_numbers(schematic)
    parts     = find_parts(schematic, numbers)
    print(sum(parts))

def find_stars(schematic: Schematic) -> Iterator[Star]:
    rows    = len(schematic)
    columns = len(schematic[0])

    for r in range(1, rows):
        for c in range(1, columns):
            token = schematic[r][c]
            if token == '*':
                yield (r, c)

def find_gears(schematic: Schematic, stars: Iterator[Star], numbers: list[Number]) -> Iterator[int]:
    for star_r, star_c in stars:
        gears = [                                                                                                                      
            int(schematic[number_r][number_c_head:number_c_tail])
            for number_r, number_c_head, number_c_tail in numbers
            if any(star_r + dr == number_r and number_c_head <= (star_c + dc) < number_c_tail for dr, dc in DIRECTIONS)
        ]
        if len(gears) == 2:
            yield gears[0] * gears[1]

def main(stream=sys.stdin) -> None:
    schematic = read_schematic(stream)
    numbers   = find_numbers(schematic)
    stars     = find_stars(schematic)
    gears     = find_gears(schematic, stars, list(numbers))
    print(sum(gears))

GitHub Repo

Another day of the 2023 Advent of Code, and another day where I hate looking at my code. This year just seems like it is starting off a lot more complex than I remember in previous years. This one was a little tricky, but I got there without any major setbacks. Another one I am excited to come back to and clean up, but this first pass is all about getting a solution, and this one works.

https://github.com/capitalpb/advent_of_code_2023/blob/main/src/solvers/day03.rs

#[derive(Clone, Copy, Debug)]
struct Location {
    row: usize,
    start_col: usize,
    end_col: usize,
}

#[derive(Debug)]
struct EngineSchematic {
    schematic: Vec>,
    numbers: Vec,
    symbols: Vec,
}

impl EngineSchematic {
    fn from(input: &str) -> EngineSchematic {
        let schematic: Vec> = input.lines().map(|line| line.chars().collect()).collect();
        let mut numbers = vec![];
        let mut symbols = vec![];
        let mut location: Option = None;

        for (row_index, row) in schematic.iter().enumerate() {
            for (col, ch) in row.iter().enumerate() {
                match ch {
                    ch if ch.is_ascii_punctuation() => {
                        if let Some(location) = location {
                            numbers.push(location);
                        }
                        location = None;

                        if ch != &'.' {
                            symbols.push(Location {
                                row: row_index,
                                start_col: col,
                                end_col: col,
                            });
                        }
                    }
                    ch if ch.is_digit(10) => {
                        if let Some(mut_location) = location.as_mut() {
                            mut_location.end_col = col;
                        } else {
                            location = Some(Location {
                                row: row_index,
                                start_col: col,
                                end_col: col,
                            });
                        }
                    }
                    _ => {
                        unreachable!("malformed input");
                    }
                }
            }

            if let Some(location) = location {
                numbers.push(location);
            }
            location = None;
        }

        EngineSchematic {
            schematic,
            numbers,
            symbols,
        }
    }

    fn get_number_value(&self, location: &Location) -> u32 {
        self.schematic[location.row][location.start_col..=location.end_col]
            .iter()
            .collect::()
            .parse::()
            .unwrap()
    }

    fn is_gear(&self, location: &Location) -> bool {
        self.schematic[location.row][location.start_col] == '*'
    }

    fn are_adjacent(&self, location: &Location, other_location: &Location) -> bool {
        location.start_col >= other_location.start_col.checked_sub(1).unwrap_or(0)
            && location.end_col <= other_location.end_col + 1
            && (location.row == other_location.row
                || location.row == other_location.row.checked_sub(1).unwrap_or(0)
                || location.row == other_location.row + 1)
    }
}

pub struct Day03;

impl Solver for Day03 {
    fn star_one(&self, input: &str) -> String {
        let schematic = EngineSchematic::from(input);

        schematic
            .numbers
            .iter()
            .filter(|number| {
                schematic
                    .symbols
                    .iter()
                    .any(|symbol| schematic.are_adjacent(symbol, number))
            })
            .map(|number| schematic.get_number_value(number))
            .sum::()
            .to_string()
    }

    fn star_two(&self, input: &str) -> String {
        let schematic = EngineSchematic::from(input);

        schematic
            .symbols
            .iter()
            .filter(|symbol| schematic.is_gear(symbol))
            .map(|symbol| {
                let adjacent_numbers = schematic
                    .numbers
                    .iter()
                    .filter(|number| schematic.are_adjacent(symbol, number))
                    .collect::>();
                if adjacent_numbers.len() == 2 {
                    schematic.get_number_value(adjacent_numbers[0])
                        * schematic.get_number_value(adjacent_numbers[1])
                } else {
                    0
                }
            })
            .sum::()
            .to_string()
    }
}

[LANGUAGE: C#]

I kept trying to create clever solutions, but ended up falling back on regex when it was taking to long. THE TLDR is we scan the list of strings for a symbol, then parse the three lines above, below and inline with the symbol for digits. Then we try and match the indexes of the match and the area around the symbol. Part 2 was a small modification, and was mostly about getting the existing code to conform the data into a pattern for each of the three lines.

Part 1

static char[] Symbols = { '@', '#', '$', '%', '&', '*', '/', '+', '-', '=' };
string pattern = @"\d+";
static List? list;
list = new List((await File.ReadAllLinesAsync(@".\Day 3\PuzzleInput.txt")));

int count = 0;
for (int row = 0; row < list.Count; row++)
{
    for (int col = 0; col < list[row].Length; col++)
    {
        var c = list[row][col];
        if (c == '.')
        {
            continue;
        }

        if (Symbols.Contains(c))
        {
            var res = Calculate(list[row - 1], col);
            res += Calculate(list[row], col);
            res += Calculate(list[row + 1], col);
            count += res;
        }

    }
}
Console.WriteLine(count);

private static int Calculate(string line, int col)
{
    List indexesToCheck = new List { col - 1, col, col + 1 };
    int count = 0;
    MatchCollection matches = Regex.Matches(line, pattern);

    foreach (Match match in matches)
    {
        string number = match.Value;

        if (AnyIndexInList(indexesToCheck, match.Index, match.Length))
        {
            count += Int32.Parse(number);
        }
    }
    return count;
}

static bool AnyIndexInList(List list, int startIndex, int length)
{
    for (int i = startIndex; i < startIndex + length; i++)
    {
        if (list.Contains(i))
        {
            return true;
        }
    }
    return false;
}

Part 2:

list = new List((await File.ReadAllLinesAsync(@".\Day 3\PuzzleInput.txt")));

int count = 0;
for (int row = 0; row < list.Count; row++)
{
    for (int col = 0; col < list[row].Length; col++)
    {
        var c = list[row][col];
        if (c == '.')
            continue;
        
        if (c == '*')
        {
            var res1 = Calculate2(list[row - 1], col);
            var res2 = Calculate2(list[row], col);
            var res3 = Calculate2(list[row + 1], col);

            count += (res1, res2, res3) switch 
            {
                {res1: not null, res2: null, res3: null } when  res1[1] != null => res1[0].Value * res1[1].Value,
                {res1:  null, res2: not null, res3: null } when res2[1] != null => res2[0].Value * res2[1].Value,
                {res1:  null, res2: null, res3: not null } when res3[1] != null => res3[0].Value * res3[1].Value,

                {res1: not null, res2: not null, res3: null } => res1[0].Value * res2[0].Value,
                {res1: not null, res2: null, res3: not null } => res1[0].Value * res3[0].Value,
                {res1: null, res2: not null, res3: not null } => res2[0].Value * res3[0].Value,
                {res1: not null, res2: not null, res3: not null } => res1[0].Value * res2[0].Value * res3[0].Value,

                _ => 0
            } ;
        }
    }
}
                
Console.WriteLine(count);


private static int?[]? Calculate2(string line, int col)
{
    List indexesToCheck = new List { col - 1, col, col + 1 };
    int?[]? count = null;
    MatchCollection matches = Regex.Matches(line, pattern);

    foreach (Match match in matches)
    {
        string number = match.Value;

        if (AnyIndexInList(indexesToCheck, match.Index, match.Length))
        {
            if (count == null)
                count = new int?[2] { Int32.Parse(number), null };
            else {
                count[1] = Int32.Parse(number);
            };
        }
    }
    return count;
}

Edit: Updated now with part 2.

Managed to have a crack at this a bit earlier today, I’ve only done Part 01 so far. I’ll update with Part 02 later.

I tackled this with the personal challenge of not loading the entire puzzle input into memory, which would have made this a bit easier.

Solution in Rust 🦀

View formatted on GitLab

use std::{
    env, fs,
    io::{self, BufRead, BufReader, Read},
};

fn main() -> io::Result<()> {
    let args: Vec = env::args().collect();
    let filename = &args[1];
    let file1 = fs::File::open(filename)?;
    let file2 = fs::File::open(filename)?;
    let reader1 = BufReader::new(file1);
    let reader2 = BufReader::new(file2);

    println!("Part one: {}", process_part_one(reader1));
    println!("Part two: {}", process_part_two(reader2));
    Ok(())
}

fn process_part_one(reader: BufReader) -> u32 {
    let mut lines = reader.lines().peekable();
    let mut prev_line: Option = None;
    let mut sum = 0;
    while let Some(line) = lines.next() {
        let current_line = line.expect("line exists");
        let next_line = match lines.peek() {
            Some(Ok(line)) => Some(line),
            Some(Err(_)) => None,
            None => None,
        };
        match (prev_line, next_line) {
            (None, Some(next)) => {
                let lines = vec![¤t_line, next];
                sum += parse_lines(lines, true);
            }
            (Some(prev), Some(next)) => {
                let lines = vec![&prev, ¤t_line, next];
                sum += parse_lines(lines, false);
            }
            (Some(prev), None) => {
                let lines = vec![&prev, ¤t_line];
                sum += parse_lines(lines, false);
            }
            (None, None) => {}
        }

        prev_line = Some(current_line);
    }
    sum
}

fn process_part_two(reader: BufReader) -> u32 {
    let mut lines = reader.lines().peekable();
    let mut prev_line: Option = None;
    let mut sum = 0;
    while let Some(line) = lines.next() {
        let current_line = line.expect("line exists");
        let next_line = match lines.peek() {
            Some(Ok(line)) => Some(line),
            Some(Err(_)) => None,
            None => None,
        };
        match (prev_line, next_line) {
            (None, Some(next)) => {
                let lines = vec![¤t_line, next];
                sum += parse_lines_for_gears(lines, true);
            }
            (Some(prev), Some(next)) => {
                let lines = vec![&prev, ¤t_line, next];
                sum += parse_lines_for_gears(lines, false);
            }
            (Some(prev), None) => {
                let lines = vec![&prev, ¤t_line];
                sum += parse_lines_for_gears(lines, false);
            }
            (None, None) => {}
        }

        prev_line = Some(current_line);
    }

    sum
}

fn parse_lines(lines: Vec<&String>, first_line: bool) -> u32 {
    let mut sum = 0;
    let mut num = 0;
    let mut valid = false;
    let mut char_vec: Vec> = Vec::new();
    for line in lines {
        char_vec.push(line.chars().collect());
    }
    let chars = match first_line {
        true => &char_vec[0],
        false => &char_vec[1],
    };
    for i in 0..chars.len() {
        if chars[i].is_digit(10) {
            // Add the digit to the number
            num = num * 10 + chars[i].to_digit(10).expect("is digit");

            // Check the surrounding character for non-period symbols
            for &x in &[-1, 0, 1] {
                for chars in &char_vec {
                    if (i as isize + x).is_positive() && ((i as isize + x) as usize) < chars.len() {
                        let index = (i as isize + x) as usize;
                        if !chars[index].is_digit(10) && chars[index] != '.' {
                            valid = true;
                        }
                    }
                }
            }
        } else {
            if valid {
                sum += num;
            }
            valid = false;
            num = 0;
        }
    }
    if valid {
        sum += num;
    }
    sum
}

fn parse_lines_for_gears(lines: Vec<&String>, first_line: bool) -> u32 {
    let mut sum = 0;
    let mut char_vec: Vec> = Vec::new();
    for line in &lines {
        char_vec.push(line.chars().collect());
    }
    let chars = match first_line {
        true => &char_vec[0],
        false => &char_vec[1],
    };
    for i in 0..chars.len() {
        if chars[i] == '*' {
            let surrounding_nums = get_surrounding_numbers(&lines, i);
            let product = match surrounding_nums.len() {
                0 | 1 => 0,
                _ => surrounding_nums.iter().product(),
            };
            sum += product;
        }
    }
    sum
}

fn get_surrounding_numbers(lines: &Vec<&String>, gear_pos: usize) -> Vec {
    let mut nums: Vec = Vec::new();
    let mut num: u32 = 0;
    let mut valid = false;
    for line in lines {
        for (i, char) in line.chars().enumerate() {
            if char.is_digit(10) {
                num = num * 10 + char.to_digit(10).expect("is digit");
                if [gear_pos - 1, gear_pos, gear_pos + 1].contains(&i) {
                    valid = true;
                }
            } else if num > 0 && valid {
                nums.push(num);
                num = 0;
                valid = false;
            } else {
                num = 0;
                valid = false;
            }
        }
        if num > 0 && valid {
            nums.push(num);
        }
        num = 0;
        valid = false;
    }
    nums
}

#[cfg(test)]
mod tests {
    use super::*;

    const INPUT: &str = "467..114..
...*......
..35..633.
......#...
617*......
.....+.58.
..592.....
......755.
...$.*....
.664.598..";

    #[test]
    fn test_process_part_one() {
        let input_bytes = INPUT.as_bytes();
        assert_eq!(4361, process_part_one(BufReader::new(input_bytes)));
    }

    #[test]
    fn test_process_part_two() {
        let input_bytes = INPUT.as_bytes();
        assert_eq!(467835, process_part_two(BufReader::new(input_bytes)));
    }
}

Only had the time to solve part 1, but had a lot of fun with it. Here’s my solution: d03/p1

[Language: Lean4]

I’ll only post the actual parsing and solution. I have written some helpers which are in other files, as is the main function. For the full code, please see my github repo.

Here I used HashMap and HashSet, but that’s just an optimization. I’m not even sure if they are faster than just using lists here…

import Lean.Data.HashSet
import Lean.Data.HashMap

namespace Day3
structure Coordinate : Type 0 where
  x : Nat
  y : Nat
  deriving Repr, BEq, Ord, Hashable

def Coordinate.default : Coordinate := {x := 0, y := 0}

/--Returns the adjacent fields, row-major order (this is important)-/
def Coordinate.adjacents : Coordinate → List Coordinate
| { x := 0, y := 0} => [
                     ⟨1,0⟩,
    ⟨0,1⟩,           ⟨1,1⟩
  ]
| { x := 0, y := y} => [
    ⟨0,y.pred⟩,      ⟨1,y.pred⟩,
                     ⟨1,y⟩,
    ⟨0,y.succ⟩,      ⟨1,y.succ⟩
  ]
| { x := x, y := 0} => [
    ⟨x.pred,0⟩,                  ⟨x.succ,0⟩,
    ⟨x.pred,1⟩,      ⟨x,1⟩,      ⟨x.succ,1⟩
  ]
| { x := x, y := y} => [
    ⟨x.pred,y.pred⟩, ⟨x,y.pred⟩, ⟨x.succ,y.pred⟩,
    ⟨x.pred,y⟩,                  ⟨x.succ,y⟩,
    ⟨x.pred,y.succ⟩, ⟨x,y.succ⟩, ⟨x.succ,y.succ⟩
  ]

structure Part : Type 0 where
  symbol : Char
  position : Coordinate
  deriving Repr

structure PartNumber : Type 0 where
  value : Nat
  positions : List Coordinate
  deriving Repr, BEq

-- Schematic is just using lists, because at this point it's not clear what kind of lookup
-- is needed in part 2... Probably some kind of HashMap Coordinate Whatever, but that's
-- guesswork for now...
-- Parts can refine the data further, anyhow.
structure Schematic : Type 0 where
  parts : List Part
  numbers : List PartNumber
  deriving Repr

/-- nextByChar gives the coordinate of the **next** character. -/
private def Coordinate.nextByChar : Coordinate → Char → Coordinate
| {x := _, y := oldY}, '\n' => { x := 0, y := oldY + 1 }
| {x := oldX, y := oldY}, _ => { x := oldX + 1, y := oldY }

private def extractParts : List (Coordinate × Char) → List Part :=
  (List.map (uncurry $ flip Part.mk)) ∘ (List.filter $ not ∘ λ (sc : Coordinate × Char) ↦ sc.snd.isWhitespace || sc.snd.isDigit || sc.snd == '.')

private def extractPartNumbers (input : List (Coordinate × Char)) : List PartNumber :=
  let rec helper := λ
  | [], none => []
  | [], some acc => [acc] -- if we are still accumulating a number at the end, commit
  | a :: as, none =>
    if p: a.snd.isDigit then
      --start accumulating a PartNumber
      helper as $ some {value := a.snd.asDigit p, positions := [a.fst]}
    else
      --not accumulating, not a digit, not of interest.
      helper as none
  | a :: as, some acc =>
    if p: a.snd.isDigit then
      --keep accumulating
      helper as $ some {value := acc.value * 10 + a.snd.asDigit p, positions := a.fst :: acc.positions }
    else
      -- we were accumulating, aren't on a number any more -> commit
      acc :: helper as none
  helper input none

def parse (schematic : String) : Option Schematic := do
  -- I think this one is easier if we don't split the input in lines. Because:
  let charsWithCoordinates ← match schematic.toList with
    | [] => none
    | c :: cs => pure $ cs.scan (λ s c ↦ (uncurry Coordinate.nextByChar s, c)) (Coordinate.default, c)
  -- Whitespaces are **intentionally** left in. This makes extracting the numbers easier.
  pure $ {
    parts := extractParts charsWithCoordinates
    numbers := extractPartNumbers charsWithCoordinates
  }

def part1 (schematic : Schematic) : Nat :=
  -- fast lookup: We need to know if a part is at a given coordinate
  open Lean(HashSet) in
  let partCoordinates := HashSet.insertMany HashSet.empty $ schematic.parts.map Part.position
  let partNumbers := schematic.numbers.filter λnumber ↦
    number.positions.any λposition ↦
      position.adjacents.any partCoordinates.contains
  partNumbers.foldl (· + PartNumber.value ·) 0

def part2 (schematic : Schematic) : Nat :=
  -- and now it is obvious that keeping the parsed input free of opinions was a good idea.
  -- because here we need quick lookup for the numbers, not the parts.
  open Lean(HashMap) in
  let numberCoordinates : HashMap Coordinate PartNumber :=
    Lean.HashMap.ofList $ schematic.numbers.bind $ λ pn ↦ pn.positions.map (·, pn)
  let gearSymbols := schematic.parts.filter (Part.symbol · == '*')
  -- but the symbols aren't enough, they need to be adjacent to **exactly** 2 numbers
  let numbersNextGearSymbols := List.dedup <$> gearSymbols.map λgs ↦
    gs.position.adjacents.filterMap numberCoordinates.find?
  let gearSymbols := numbersNextGearSymbols.filter (List.length · == 2)
  let gearRatios := gearSymbols.map $ List.foldl (· * PartNumber.value ·) 1
  gearRatios.foldl (· + ·) 0

Python solution

just more parsing problems