A Lean 4 formalization of the Umans–Lenhart polynomial-time algorithm for the Hamiltonian cycle problem on solid grid graphs (grid graphs without holes). It covers the existence of alternating strip sequences, the algorithm itself, its correctness, and a polynomial bound on its running time.

theorem ULHC.ulhc_main {V : Finset Pt} (hs : Solid V) :
    ((T.ulhcT V).ret = true ↔ ∃ H, Deg2 V H ∧ ncomp V H = 1) ∧
      (T.ulhcT V).time ≤ 500000000 * (V.card + 1) ^ 12

For a solid set of lattice points V, the algorithm returns true exactly when the grid graph on V has a Hamiltonian cycle (a 2-factor with one component), and it takes at most 5·10⁸·(|V|+1)¹² steps. T.ulhcT is the algorithm written in a step-counting monad; its result is proved equal to the plain algorithm ulhc.

• No sorry. The main results use only propext, Classical.choice and Quot.sound.
• The build has no warnings.

docs/MAP.md maps the thesis and paper statement by statement to Lean names, and lists where the proof departs from the source and the gaps found in the source.

Lean checks everything except the following:

• The definitions in the statement: Pt, IsEdge, Deg2, ncomp and Solid (lean/ULHC/Grid.lean, StripCount.lean, Graph.lean). Solid is cross-checked against "all interior faces have unit area" by checks/solid_check.py and checks/solid_check_grid.py.
• The cost model: the table of basic-operation costs at the top of lean/ULHC/Timed/TimeM.lean.
• The cost-model lint: checks/timed_lint.py confirms that the counted algorithm uses only those operations.

You need elan. The toolchain (lean/lean-toolchain, Lean v4.35.0-rc2) and Mathlib (lean/lake-manifest.json) are pinned.

cd lean
lake exe cache get
lake build

lean/build.sh wraps lake build. On a shared machine, ULHC_MEM=8G LEAN_NUM_THREADS=2 lean/build.sh caps memory (through systemd-run) and threads.

scripts/check.sh

This builds with warnings treated as errors, checks the axioms of the main results (lean/CheckAxioms.lean), and runs the cost-model lint.

scripts/sanity.sh

This evaluates ulhc with Lean on small solid sets and compares it with a brute-force Hamiltonian cycle search. It also re-runs the cross-checks of Solid. The results of larger runs are in docs/MAP.md.

• lean/ULHC/: the formalization (19k lines).
  • Main.lean: ulhc_main.
  • TheoremA.lean, V2Seq.lean: strip sequences exist.
  • Algorithm.lean, LinkGraph.lean, MinPath.lean: the algorithm.
  • NearCA.lean, PathComplete.lean, AlgComplete.lean: one round, completeness, termination.
  • Timed/, Cost*.lean: the counted algorithm and its step bounds.
• docs/: the statement map, as Markdown (MAP.md) and as a web page (map.html).
• checks/: the cost-model lint, the sanity checks, and probes/ (exploratory scripts from the development, not maintained).
• BLUEPRINT.md: the working log of the formalization.
• scripts/: check.sh, sanity.sh.

• C. Umans, An algorithm for finding Hamiltonian cycles in grid graphs without holes, B.A. honors thesis, Williams College, May 1996.
• C. Umans and W. Lenhart, Hamiltonian cycles in solid grid graphs, Proc. 38th FOCS, 1997, pp. 496–505.

The paper also claims the result for quad-quad graphs. That extension is not formalized here, and the sources give no separate proof of it.

The Lean code and the probe scripts were written by Claude, Opus 5.5 (Anthropic), under the direction of the repository owner.

CC0 1.0 Universal: dedicated to the public domain.