4 ms·
It is vastly easier to do the formalization than to actually solve the problem. Any undergraduate with some lean familiarity could do it in minutes.
by sebzim4500 2y ago
It is vastly easier to do the formalization than to actually solve the problem. Any undergraduate with some lean familiarity could do it in minutes.
- Davidzheng 2y agoDisagree! Some problems are much harder than others. If you don't believe me please go formalize P5 in this year imo.
- sebzim4500 2y agoYeah, I was just referring to the problems that it actually did.
- SonOfLilit 2y agoI 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)})
- Davidzheng 2y agoI 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.
- SonOfLilit 2y agoFormalization is mechanical work, lets leave it for computers to do :)
- Davidzheng 2y agoI completely agree