发表机构
Eindhoven University of Technology (TU/e)（埃因霍温理工大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文证明了 Lehmer 关于多重集置换的相邻交换图存在非完美哈密顿遍历的猜想，通过将单词划分为超立方体并沿生成树粘合哈密顿环，辅以两个有限显式环，并用 Python 验证和 Lean 4 形式化证明。
AI 中文摘要
1965年，D. H. Lehmer 猜想：每个多重集的置换都允许通过相邻交换实现一个非完美的哈密顿遍历，即在相邻交换图中访问每个单词的一条路径，其中某些单词被访问两次，以便到达一个邻居并返回。该问题在 Knuth 的《计算机程序设计艺术》中被列为未解决的研究问题。Verhoeff（2017）选择了口吃单词（其中每个多米诺骨牌都是双重的）作为以这种方式到达的单词，并将该猜想重新表述为关于非口吃单词的图 $N(S)$ 的哈密顿性，但有两个例外族——具有奇数重数的二元签名，以及 $(2k,1,1)$ 的置换——它们具有哈密顿路径但没有环。本文证明了重新表述后的猜想，并由此证明了 Lehmer 猜想。关键结构是将单词划分为超立方体：多米诺骨牌内部的交换将具有相同多米诺内容的每类单词变成超立方体，而口吃单词正好是零维类。当每个重数都是偶数时，超立方体的哈密顿环沿着一棵生成树粘合，无需有限检查。恰好有一个奇数重数的情况归结为全偶数情况以及 Stachowiak（1992）的一个定理，这是唯一继承的哈密顿性输入，它也解决了两个或更多奇数重数的情况。唯一的有限成分是两个显式环，分别包含 28 和 84 个单词。每个构造都用 Python 实现，并针对暴力图进行了检查，证明在 Lean 4 中基于 Mathlib 形式化。
英文摘要
In 1965, D. H. Lehmer conjectured that the permutations of every multiset admit an imperfect Hamiltonian traversal by adjacent swaps: a walk in the neighbor-swap graph that visits every word, with some words visited twice in order to reach a neighbor and return. The question is posed as an unsolved research problem in Knuth's Art of Computer Programming. Verhoeff (2017) chose the stutter words, in which every domino is a double, as the words to be reached this way, and reformulated the conjecture as the Hamiltonicity of the graph $N(S)$ on the non-stutter words, with two exceptional families --- binary signatures with an odd multiplicity, and the permutations of $(2k,1,1)$ --- that admit a Hamiltonian path but no cycle. This article proves the reformulated conjecture, and with it Lehmer's conjecture. The key structure is a partition of the words into hypercubes: the swaps inside dominoes turn each class of words with the same domino contents into a hypercube, and the stutters are exactly the $0$-dimensional classes. When every multiplicity is even, Hamiltonian cycles of the hypercubes are glued along a spanning tree, with no finite check. The case of exactly one odd multiplicity reduces to the all-even case and to a theorem of Stachowiak (1992), the one inherited Hamiltonicity input, which also settles two or more odd multiplicities. The only finite ingredients are two explicit cycles, of 28 and 84 words. Every construction is implemented in Python and checked against brute-force graphs, and the proof is formalized in Lean 4 over Mathlib.
Comments29 pages, 3 figures
