Hamiltonian paths in rectangular grid graphs (Itai, Papadimitriou and Szwarcfiter)
A Lean 4 proof of the characterization of Hamiltonian paths in rectangular grid graphs by Itai, Papadimitriou and Szwarcfiter (1982, Theorem 3.2). For distinct vertices s and t of the width × height grid graph, a Hamiltonian path from s to t exists if and only if the problem is acceptable, that is, colour compatible (by the checkerboard colouring) and not one of the three forbidden configurations F1, F2, F3 on grids of width or height 1, 2 or 3. Necessity is proved for each forbidden case, where the paper only says "a straightforward case analysis". Sufficiency is proved by strong induction…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-22-000014
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000014/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000014/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'