Claude's Cycles

Reference: Claude's Cycles by Donald E. Knuth (2026)

Fix m ≥ 2. Consider the directed graph with vertex set (ZMod m)³, where from each vertex (i, j, k) there are directed arcs to (i+1, j, k), (i, j+1, k), and (i, j, k+1) (arithmetic mod m). The goal is to partition all 3m³ directed arcs into three edge-disjoint directed Hamiltonian cycles (each of length m³).

Knuth describes an explicit construction, found by Claude (Anthropic), that achieves this decomposition for all odd m ≥ 3. The case m = 2 is known to be impossible [Aub82]. The even case m > 2 remains open.

References

• [Knu26] D. E. Knuth, "Claude's Cycles" (2026).
• [Aub82] J. Aubert, B. Schneider, "Graphes orientés indécomposables en circuits hamiltoniens", J. Combin. Theory Ser. B 32 (1982), 347–349.

@[reducible, inline]

abbrev ClaudesCycles.Vertex (m : ℕ) : Type

The vertex type: vectors in (ZMod m)³.

Equations

• ClaudesCycles.Vertex m = (Fin 3 → ZMod m)

def ClaudesCycles.bumpAt {m : ℕ} [NeZero m] (b : Fin 3) (v : Vertex m) : Vertex m

Bump coordinate b of vertex v: add 1 to the b-th component.

Equations

• ClaudesCycles.bumpAt b v = Function.update v b (v b + 1)

def ClaudesCycles.cubeAdj {m : ℕ} [NeZero m] (u v : Vertex m) : Prop

Adjacency in the cube digraph: u is adjacent to v if v is obtained from u by bumping one coordinate.

Equations

• ClaudesCycles.cubeAdj u v = ∃ (b : Fin 3), ClaudesCycles.bumpAt b u = v

def ClaudesCycles.IsDirectedHamiltonianCycle {V : Type u_1} [Fintype V] [DecidableEq V] (adj : V → V → Prop) (σ : Equiv.Perm V) : Prop

A permutation σ on vertices is a directed Hamiltonian cycle of a digraph with adjacency adj if every arc (v, σ v) is an edge, σ is a single cycle, and σ moves every vertex.

Equations

• ClaudesCycles.IsDirectedHamiltonianCycle adj σ = ((∀ (v : V), adj v (σ v)) ∧ σ.IsCycle ∧ σ.support = Finset.univ)

def ClaudesCycles.HasHamiltonianArcDecomposition (m : ℕ) [NeZero m] : Prop

The arcs of the cube digraph on (ZMod m)³ can be decomposed into three directed Hamiltonian cycles: there exist three permutations, each forming a directed Hamiltonian cycle, such that every arc (v, bumpAt b v) belongs to exactly one cycle.

Equations

• One or more equations did not get rendered due to their size.

theorem ClaudesCycles.cube_hamiltonian_arc_decomposition {m : ℕ} [NeZero m] (hm : Odd m) (hm' : 1 < m) : HasHamiltonianArcDecomposition m

For odd m > 1, the cube digraph on (ZMod m)³ has a Hamiltonian arc decomposition into three directed cycles [Knu26].

theorem ClaudesCycles.cube_hamiltonian_arc_decomposition_impossible_m2 : ¬HasHamiltonianArcDecomposition 2

The case m = 2 is impossible: the cube digraph on (ZMod 2)³ does not have a Hamiltonian arc decomposition [Aub82].

theorem ClaudesCycles.cube_hamiltonian_arc_decomposition_even : True ↔ ∀ (m : ℕ) (x : NeZero m), Even m → 2 < m → HasHamiltonianArcDecomposition m

For even m > 2, it is open whether the cube digraph on (ZMod m)³ has a Hamiltonian arc decomposition.