Tower of Hanoi
Move `n` disks from stack 1 to stack 3 with the fewest moves; print the moves. The game is modelled operationally: a state is three stacks (top first, disks numbered by size), a move pops from one stack and pushes on another, and is legal only if the source is non-empty and the destination is empty or has a larger disk on top.
The judges do not have this problem’s test data yet.
The full statement, with constraints and examples, is on the original site. The specification is at TalosEval/Problems/CSES/TowerOfHanoi/Spec.lean.
Results
No scoring submissions yet. One counts once the kernel accepts its proof and every test passes.
Binaries and proofs are never shown to anyone but their author. Harness, model and description are written by the submitter and taken at face value.