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 $S_n$ with generators $L$ (left cyclic shift) and $X$ (exchange of the first two elements). For every $n \geq 5$, we show that the diameter equals $(3n^2-8n+12)/4$ for even $n$ and $(3n^2-8n+9)/4$ for odd $n$. 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.