Yeah, I was just referring to the problems that it actually did.

I formalized it last night, to a level that an IMO trainer agreed was adequate. Took maybe 15 minutes.

Find n such that p(n) and not p(n-1).

  p(n):
    exists(f: state -> move) such that solves(f, n)
  
  state: solved | illegal | (k, is_first_move in {T,F}, px in (1,2023), py in (1,2024+1), mapping from x,y to {T,F, ?})
  
  initial_state(n): (n, T, 1, 1, {(x,y) -> ?})
  
  move: U|D|L|R|(x in (1,2023))
  
  power: ((a -> a), integer) -> (a->a)
  power(h, 0)(x) = h(x)
  power(h, k)(x) = h(power(k-1))(x)
  
  solves(f, n): exists l such that for every board, power(make_move(board, f), l)(initial_state(n)) = solved
  
  board: permutation of (1, 2, 3, ..., 2022+1)
  
  make_move: (board, (state -> move)) -> (state -> state)
  make_move(board, f)(solved): solved
  make_move(board, f)(illegal): illegal
  make_move(board, f)(s = (k, is_first_move, px, py, m))
     if is_first_move = T:
        if k = 0:
            illegal
        else if f(s) is a number:
            (k, F, f(s), 1, m)
        else:
            illegal
    else:
        if f(s) is a number:
            illegal
        else if py = 2025:
            solved
        else if board(px) = py and py != 1:
            (k - 1, T, px, py, m + {((px, py), T)})
        else:
            dy = {U:-1,D:1,L:0,R:0}(f(s))
            dx = {U:0,D:0,L:-1,R:1}(f(s))
            px' = px+dx
            py' = py+dy
            if px' < 1 or px' > 2023 or py' < 1 or py' > 2025:
                illegal
            (k, F, px', py', m + {((px, py), F)})

I find it incredibly impressive you did this in 15 minutes! You should really help out in formalizing math (completely serious).

Personally in the past I tried a few times to formalize some statements and sometimes I found that the mathlib libraries were pretty lacking in these more open-ended problems (I wanted to reason about lists and stuff). But it seems that I am just very bad at formalization lol.

Formalization is mechanical work, lets leave it for computers to do :)

I completely agree