{"id":"palomar/PALOMAR-2026-10-19-000001","url":"https://github.com/zzyzek/SolidGridGraphHamPath/tree/2bacb1aa9851ed6c653dbc8b33044e898f0baecc/lean","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-19-000001-v1.json","repo":"https://github.com/zzyzek/SolidGridGraphHamPath","tags":["cs.DM","cs.CC","msc:05C45","msc:68R10","msc:68Q25","grid-graphs","hamiltonian-paths","lean"],"score":0,"title":"Hamiltonian s–t paths in solid grid graphs are decidable in polynomial time","trust":"high","domain":"cs.DM","source":"palomar","authors":["Z. Zzyzek"],"reviews":0,"subject":"cs.DM","summary":"A computable algorithm, decideHamPath, that decides whether a solid grid graph (a finite set of lattice points with no holes, with an edge between points at distance 1) has a Hamiltonian path between two given distinct points, with a Lean 4 proof that it is correct. The problem was posed by Itai, Papadimitriou and Szwarcfiter (1982). The algorithm extends Sheffield's height-function algorithm for Hamiltonian cycles: each endpoint gets a phantom edge to a missing neighbour, and an endpoint with all eight neighbours present becomes a hole whose defect (a vortex) is handled by a slit height and…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-19","reactions":{},"formalized":true}