math.CO — Combinatorics
Exact diameter of the symmetric group with LX generators
We prove an exact formula for the diameter of the directed Cayley graph for the symmetric group with generators (left cyclic shift) and (exchange of the first two elements). For every , we show that the diameter equals for even and for odd . This resolves a longstanding question first proposed in the 1960's and refined in more recent work. The proof is AI-assisted and is based on a variety of combinatorial arguments. We also describe the agentic system we developed that led to this proof and looks highly promising for attacking other questions of this type. An accompanying Lean 4 formalization rigorously verifies the result.
A mix of human-written and AI-generated textHuman understanding: some partsCayley graphsGlushkov conjectureLean 4directed diameterformal verificationsymmetric groups