Claude's cycles: decomposing a 3D torus digraph into Hamiltonian cycles

Claude Opus 4.6 found a construction that splits a digraph from Knuth's forthcoming TAOCP section into three Hamiltonian cycles for every odd m; Knuth proved it and it was formalized in Lean. The even case has a separate, unverified AI proof.

Problem
For every m>2m > 2, can the arcs of the digraph on vertices ijkijk (arcs increase ii, jj or kk by 1 mod mm) be split into three directed Hamiltonian cycles?
Credit
Claude Opus 4.6 (Anthropic), coached by Filip Stappers; proof by Donald Knuth · Human-guided AI exploration; human proof
Checked
Proof written by KnuthLean formalization (Kim Morrison)
Timeline
Knuth's note 2026-02-28, revised 2026-04-14
Sources
Knuth, “Claude's Cycles”Lean formalization
SOLVEDOdd m: proved and Lean-checked

The problem

The digraph has the m3m^3 vertices ijkijk with 0≤i,j,k<m0 \le i, j, k < m, and from each vertex an arc that increases ii, jj or kk by 1 modulo mm. The question, which arose in Donald Knuth's draft section on Hamiltonian cycles for The Art of Computer Programming, is whether its arcs can be split into three directed Hamiltonian cycles for every m>2m > 2. For m=2m = 2 it is impossible.

What AI did

Filip Stappers posed the problem to Claude Opus 4.6 and coached it through a series of explorations. On the 31st, Claude produced a construction that worked for every odd mm from 3 to 11; Stappers then tested it for every odd mm up to 101. Knuth described the episode in a note titled "Claude's Cycles" (28 February 2026, revised 14 April 2026), and counted exactly 760 "Claude-like" decompositions that work for all odd mm.

How it was checked

Knuth wrote the rigorous proof for all odd mm himself, and Kim Morrison formalized it in Lean.

Limitations

The record covers the odd case. For even mm, Claude made only partial progress; Ho Boon Suan's code written with gpt-5.3-codex covers even m≥8m \ge 8 (tested up to 2000), and GPT-5.4 Pro then wrote a 14-page proof that Knuth calls "apparently flawless" but that has not been independently verified. This is a research problem from Knuth's book, not a long-standing famous conjecture.

∎