Hamiltonian s–t paths in solid grid graphs

A demo of the polynomial-time decision procedure whose correctness and step bound are proved in Lean 4 (decideHamPath_main). This page runs the JavaScript port of its fast mode. Click a lattice point to add or remove it, or choose s / t below and click to place an endpoint. The shape must be solid (no holes).

The path is coloured from blue at s to orange at t; points are black or white by the parity of x+y. With the heuristic off, every answer comes from the algorithm itself. Large shapes (a few hundred points) can take a few seconds.