Glushkov's L/X problem (Glushkov 1968) asks for the largest number of moves needed to rearrange a permutation of 
objects using two operations. The operation 
shifts the list cyclically one place to the left, and 
exchanges its first two positions. Each
operation costs one move. A right shift therefore costs 
applications of 
, rather than one move. The problem
is the directed graph diameter of the Cayley
graph of the symmetric group 
generated by these two operations. With the convention 
, the diameters for 
, 2, ... begin 0, 1, 2, 6, 11, 18, 25, 35, 45, 58,
71, ... (OEIS A039745).
Uskov et al. (2026a) reported the exact formula
 |
(1)
|
for every 
. For example, 
, 
, 
, and 
. The authors credit an
agent system using GPT-6 Astra and Codex with generating the proof
and its Lean formalization (Uskov et al. 2026a). The version 1.0.1 release
includes a separate statement of the exact all-pairs directed graph
diameter and a bound on the length of an L/X word taking any permutation
to any other. The release's public Comparator run checked the proofs
against these statements, and its axiom audit reported only standard Lean axioms
(Uskov et al. 2026b). Palomar (2026) records separate machine checks of the
two statements at an earlier revision.
