Lehmer's 1965 permutation conjecture (a research problem in Knuth's TAOCP) proved; Claude Opus 5.5 found the short hypercube proof
On Oct 1, 2026 Tom Verhoeff posted a proof of D. H. Lehmer's 1965 conjecture that the permutations of every multiset admit an imperfect Hamiltonian traversal by adjacent swaps. Knuth's The Art of Computer Programming lists the question as an unsolved research problem. After about six months of work with earlier Claude models had produced a proof of nearly 200 pages, Claude Opus 5.5 found a short proof "within a couple of hours", built on a partition of the words into hypercubes. Harmonic's Aristotle produced the Lean formalization.
Key facts
- arXiv 2610.01240 (math.CO), Tom Verhoeff, 'A proof of Lehmer's permutation conjecture for neighbor-swap graphs', Oct 1, 2026
- Result: proves Verhoeff's 2017 reformulation, Hamiltonicity of the graph N(S) on non-stutter words, with two exceptional families that have only Hamiltonian paths. This implies Lehmer's conjecture
- AI role (paper): 'In that study phase, Claude Opus 5.5 proposed the representation that became the partition into hypercubes … It then developed this lead into the two theorems above, in successive multi-agent rounds: writing, independent recomputation of every construction, adversarial red-teaming, and hand refereeing'
- Acknowledgments: 'I worked with various Claude models — Opus 4.7, Opus 4.8, Fable 5 (and Fable 5.1), and Opus 5 — but progress was slow; after some six months the proof (then almost 200 pages of dense mathematics) and its Lean formalization (more than one hundred thousand lines) came together. Then Opus 5.5 appeared, and Anton asked it to come up with a simple proof from scratch, which it did within a couple of hours.'
- 'The hypercube proof at the heart of this article was found and developed by Claude Opus 5.5 in a multi-agent proof effort.' Harmonic's Aristotle produced the Lean formalization
- The problem was restarted after Anton Bakker's March 2026 challenge, made when Opus 4.7 came out: 'Software is done, and I bet mathematics as well'
Science result
- Field
- mathematics / combinatorics (Gray codes, Hamiltonian cycles in Cayley-type graphs)
- Problem
- Lehmer's permutation conjecture (1965): imperfect Hamiltonian traversals of multiset permutations by adjacent swaps; an unsolved research problem in Knuth's TAOCP (open since 1965)
- Result
- Proof of Verhoeff's reformulation (Hamiltonicity of the non-stutter-word graph N(S), with two exceptional families), and hence of Lehmer's conjecture.
- AI system
- Claude Opus 5.5, Aristotle
- Human role
- Human-led long project; the final short proof was found and developed by Claude Opus 5.5 in a multi-agent setup, then re-derived and checked by the author
- Verification
- Lean formalization by Harmonic's Aristotle (per the paper); unrefereed preprint
- Status
- pending
- Why surprising
- Six months of work with earlier models gave a ~200-page proof; Opus 5.5 found a short one from scratch in a couple of hours.
What happened
D. H. Lehmer conjectured in 1965 that the permutations of any multiset can be traversed by adjacent swaps, visiting every word, with some words visited twice. Knuth's TAOCP lists it as an open research problem. In 2017 Verhoeff restated it as a Hamiltonicity question. Working with successive Claude models from March 2026, he first reached a very long proof. Then Claude Opus 5.5 proposed reading each word as a sequence of "dominoes". In that view the even-position swaps generate hypercube orbits, and gluing their Gray cycles gives the Hamiltonian cycles. A multi-agent workflow developed this into the paper's main theorems.
Why it matters
This is a famous, decades-old combinatorics problem named in Knuth's TAOCP, and the paper credits the key proof idea directly to Claude Opus 5.5. It is also a clear before-and-after comparison: earlier models helped produce a long proof slowly, while the newer model found a short one quickly. The result is still an unrefereed preprint, so its status is pending.
Changelog
- 2026-10-02: created from sweep 2026-10-02 (AI disclosure read in the PDF)
Related events
- Summer 2026 flood: dozens of named conjectures settled on arXiv with disclosed AI help (July–September catalogue) ★★★★
- Donald Knuth's 'Claude's Cycles': Claude Opus 4.6 solves an open Hamiltonian-cycle problem ('Shock! Shock!') ★★★★
Sources (1)
id: 2026-10-01-lehmer-permutation-conjecture-opus-5-5 · updated 2026-10-02 · open in the interactive timeline