Materials

What the work was done with, as its author lists it, so someone else can get the same things and do it again.

Software
Lean 4 theorem prover, version 4.34.1
github.com/leanprover/lean4
Checks proofs/SB3.lean with its core library only; pinned in env/Dockerfile and env/lean-toolchain.
Software
Python
python.org · RRID:SCR_008394
Runs code/gen_traces.py, which generated the first-return lemmas of the proof; standard library only, Python 3.10 or later.

Study

Opening the study…

Materials: A simple successor rule gives a Hamiltonian cycle in Knuth's shift-and-save-or-bump digraph SB(m, 3) for every m > 1 · sciencejournal.ai