Polynomial-time Hamiltonian s-t paths in solid grid graphs
A grid graph is a finite set with an edge between every two points at distance ; it is solid if it has no holes. Itai, Papadimitriou and Szwarcfiter (1982) showed that deciding whether a grid graph has a Hamiltonian path between given vertices and is NP-complete, and that it is solvable in linear time for rectangular grid graphs. Umans and Lenhart (1997) gave a polynomial-time algorithm for Hamiltonian cycles in solid grid graphs. Is there a polynomial-time algorithm that decides, for a solid grid graph and distinct , whether has a Hamiltonian path from to ?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Algorithmic graph theory; Hamiltonian paths in grid graphs
- Posed by
- Implicit in Itai, Papadimitriou and Szwarcfiter (SIAM J. Comput. 1982), who asked the hole-free question for cycles; the path case is stated open later, e.g. by Keshavarz-Kohjerdi and Bagheri (2016).
- Year posed
- —
- Years open
- —
- Solved
- 2026-10-19
- Model
- Claude Opus 5.5
- Vendor
- Anthropic
- Collaborators
- —
- Verification
- Unreviewed
- Publication
- Announced
- Significance
- 22 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Claims a polynomial-time decision procedure, extending Sheffield's height-function method for Hamiltonian cycles: each endpoint gets a phantom edge, and an endpoint with all eight neighbours present becomes a vortex handled by slit heights and flip classes. Lean proves the algorithm correct and proves a step bound of for a cost model written beside it; the cost model's faithfulness is checked by reading, not by Lean. The Umans-Lenhart cycle algorithm is also formalised.
What the AI did
According to the repository README, Claude (Opus 5.5) did nearly all of the work: the algorithm, the paper, reference implementations in C, Python and JavaScript, the browser demo and the Lean 4 proof. The human author, zzyzek, supplied the problem statement and guidance.
Verification
Read by this site on 3 November 2026, not rebuilt. The headline theorem decideHamPath_main in lean/SolidGridHam/Path/HPFinal.lean states, for solid V and distinct s, t in V, that decideHamPath V s t = true exactly when some edge set has degree 1 at s and t, degree 2 elsewhere and one component, and that decideHamPathCost V s t is at most 5,220,000 (|V|+3)^6. The 160 Lean files contain one sorry, the deliberate hole in Challenge.lean, and no axiom declarations, admit, native_decide, unsafe or implemented_by. The axiom printout is the author's; there is no Lean CI. The Palomar entry PALOMAR-2026-10-19-000001 registers only the correctness theorem decideHamPath_correct, at commit 2bacb1a; no Lean file has changed since. Correctness alone does not settle the question, since an exponential search is also correct. The polynomial half rests on cost functions written beside the algorithm, whose match to it the README says is checked by reading, not by Lean, so the anchored statement does not cover the claim. Solid is defined by king-move escape of missing points, which matches no holes. No independent expert has checked it. Unreviewed rather than Lean-checked: the formal statement covers correctness only, and the polynomial bound, which is the claim, is not formalised.
Sources
- PaperItai, Papadimitriou and Szwarcfiter, Hamilton paths in grid graphs (1982)Umans and Lenhart, Hamiltonian cycles in solid grid graphs (FOCS 1997)Path case stated open: Hamiltonian paths in C-shaped grid graphs
- Lean statementHeadline theorem decideHamPath_main
- Palomar listingpalomar
- CodeGitHub
- OtherGithub pagesInteractive demo
Submitted by JollyCobra234 on