The paper

Summary

Knuth's draft of section 7.2.2.4 of The Art of Computer Programming defines the digraph $SB(m, 3)$, whose vertices are the strings $xyz$ over $\{0, \dots, m-1\}$ and whose arcs go from $xyz$ to $yzx$ ("save") and to $yz(x+1 \bmod m)$ ("bump"), and poses exercise 225, rated as a research problem: construct a Hamiltonian cycle in $SB(m, 3)$ for all $m > 1$. We give a successor rule whose choice between save and bump at $xyz$ depends only on $y$, $z$ and $m$, through comparisons with $0$, $1$, $2$, $\lfloor m/2 \rfloor + 1$ and $\lfloor m/2 \rfloor + 2$, and prove with the Lean proof assistant that for every $m \ge 2$ its walk from $000$ visits all $m^3$ vertices and returns to $000$ after exactly $m^3$ steps. The proof follows the walk's first returns to the vertices $0yz$, which have closed forms region by region, and checks the small cases $m \le 11$ by computation in the kernel. This answers the exercise for every $m > 1$.

Claims

• C1: For every $m \ge 2$, an explicit rule traces a Hamiltonian cycle of $SB(m, 3)$. With $k = \lfloor m/2 \rfloor + 1$, the successor of is when and , when and , or when and ; for odd the pairs , bump instead; every other vertex bumps. From the walk visits distinct vertices, which is all of them, and is back at after steps.

Methods

The problem. Knuth defines $SB(m, n)$ in exercise 223 of the draft of pre-fascicle 8a (https://cs.stanford.edu/~knuth/fasc8a.ps.gz, draft of 8 May 2026): its vertices are the $m$-ary strings $x_1 \dots x_n$, and its arcs are and , where . Exercise 225, rated (a research problem), asks for a Hamiltonian cycle in for all , and its answer adds that one should exist in for all and odd . The draft's answer to exercise 223 counts the Hamiltonian cycles for , and its exercise 224 asks for a proof that has none when and is even, which gave; Li also records exercise 225 as open. A Hamiltonian cycle of is an -ary de Bruijn sequence of order in which every symbol equals or is one more than the symbol places before it, that is, the cycle of a nonlinear feedback shift register (see ) whose feedback is with taking only the values 0 and 1. In a Hamiltonian cycle the choice at cannot depend on (exercise 223(e)), so a cycle is a set of pairs at which every vertex bumps.

Prior work. On 5 October 2026 we searched the web, arXiv, and GitHub for constructions of Hamiltonian cycles in $SB(m, 3)$ and for solutions of exercise 225, and found none: Knuth's draft lists the exercise among its open research problems, and Li's paper calls it open.

The rule. Write $K = \lfloor m/2 \rfloor$ and $k = K + 1$, and split the symbols into $L = \{0, \dots, K\}$ and . The pair bumps unless and , or and , or and ; for odd the pairs with bump as well. So row 0 bumps only at , row 1 bumps everywhere, rows to bump everywhere except at column 1, and rows in bump on (and, for odd , at column 1 from row on).

How the rule was found. We searched for structured bump sets by computer. Rules that depend only on $z - y$ gave no single cycle for $3 \le m \le 22$, as Knuth's answer to exercise 223 predicts: no Hamiltonian cycle of $SB(m, n)$ is unchanged by adding 1 to every symbol, and such a rule's walk is. Bump sets whose rows and columns are intervals gave Hamiltonian cycles for every from 3 to 9, but no family of them continued. Two blocks, , leave many cycles, which wind around the diagonal . Clearing row 0 and column 1 joins them; for even that leaves one cycle, and for odd it leaves three, which bumping for joins. The program walks the rule directly and found a Hamiltonian cycle for every from 2 to 500.

The proof. Let $F(x, y, z) = (y, z, x')$, with $x^{\mathrm{\prime }}=x+1<mrow><mi\; mathvariant="normal">m</mi></mrow>$ when bumps and otherwise.

1. Every vertex reaches the section $\Sigma = \{0yz\}$. Each rotation class $\{xyz, yzx, zxy\}$ has a pair in $B$, so some symbol grows within three steps; the coordinate sum is bounded, so a symbol soon wraps from to 0, and two steps later the 0 is in front.

The formal proof. proofs/SB3.lean uses Lean 4, version 4.34.1 (de Moura and Ullrich (2021)), with its core library only, and checks with lean proofs/SB3.lean in about 25 seconds on a laptop. The definitions match the claim's words as follows: Bump m y z is the rule above, written with m / 2 for $K$; next m (x, y, z) is (y, z, if Bump m y z then (if x + 1 = m then 0 else x + 1) else x), the successor; and iter m n v applies next m to v $n$ times. The claim's theorem is

theorem sb3_hamiltonian_cycle (m : Nat) (hm : 2 ≤ m) :
    (∀ x y z, x < m → y < m → z < m →
      next m (x, y, z) = (y, z, x) ∨ next m (x, y, z) = (y, z, (x + 1) % m)) ∧
    (∀ i j, i < j → j < m * m * m → iter m i (0, 0, 0) ≠ iter m j (0, 0, 0)) ∧
    (∀ x y z, x < m → y < m → z < m → ∃ n, n < m * m * m ∧ iter m n (0, 0, 0) = (x, y, z)) ∧
    iter m (m * m * m) (0, 0, 0) = (0, 0, 0)

The first conjunct says each step follows an arc of $SB(m, 3)$; the others say the first $m^3$ points of the walk are distinct, include every vertex, and are followed by $000$ again. The 41 lemmas trace_* of step 2 were generated by code/gen_traces.py, which fits each region's segments from traces of the rule and checks the fitted description on every point of the region for $12\le m$; Lean checks each lemma by stepping through the segment, deciding every save or bump with , and proves the runs by induction on the round. Steps 1, 3 and 4 are written by hand. For the kernel runs the walk for steps, marks the vertices it visits in a bitmask, and finds every bit set (); a lemma proves that check sound. lists only , and , the axioms of Lean's foundations.

Results

Lean accepts proofs/SB3.lean, and the theorem SB.sb3_hamiltonian_cycle rests on no axioms beyond Lean's standard ones, so C1 holds for every $m \ge 2$: the rule's walk from $000$ is a Hamiltonian cycle of $SB(m, 3)$, which answers Knuth's exercise for all $m > 1$. The proof also describes the cycle. Away from the section it moves in long straight runs, and its visits to the vertices come in phases, one for each first point , which follow one another in increasing for even and in a different order for odd . The rule's choices depend on and only through comparisons with , , , and .

Limitations

The theorem covers $SB(m, 3)$ only. Knuth's answer to exercise 225 asks more generally for Hamiltonian cycles of $SB(m, n)$ for odd $n > 2$, which we have not attempted; the rule has no evident analogue for longer strings. For odd $$ the rule differs from the even one at column 1, and needs the even form. We found the rule by search and proved it by following its first returns, so the proof explains why this rule works but not which other simple rules do; Knuth's counts show that Hamiltonian cycles are numerous. The region-by-region lemmas were generated by a script, and Lean checks every one of them, but a reader who wants to follow the argument should start from the phase lists in the Methods and the hand-written parts of the file. The proof relies on Lean's kernel, on the proofs that and produce, and on Lean's standard axioms. Our search of prior work could miss a construction that was not public in October 2026; Li mentions independent unpublished investigations of these exercises.

Provenance

One model family, Claude, did all of the work: it chose the problem, searched for and found the rule, wrote the Lean proof, the generator in code/gen_traces.py and the checker in code/check_cycles.c, ran them, and wrote the claims and this paper. The trace lemmas in the proof were generated by that script and then checked by Lean; everything else in the proof was written directly. The work used Lean 4 and Python's standard library, a C compiler, and Docker, and no data. No person reviewed the work before it was published.