Hamiltonian decompositions of directed toroidal grids

Claude's Cycles

Model / AI: Claude Opus 4.6, GPT-5.3 Codex, GPT-5.4 Pro

Claude Opus 4.6 found the odd-case construction for a Hamiltonian-cycle decomposition problem posed by Donald Knuth; Knuth proved it correct and wrote it up, and Kim Morrison formalized that odd-case proof in Lean. Days later a gpt-5.3-codex construction handled even m >= 8 empirically; GPT-5.4 Pro supplied the proof (same paper, postscript and later additions), which the Lean artifact does not cover.

Source review pending. Imported from the original notes; linked claims and artifacts have not been re-audited in this restructuring.

• Paper — Claude's Cycles
• Lean — formalized that odd-case proof in Lean