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. (2026) reported the exact formula
 |
(1)
|
for every 
.
For example, 
,
,
,
and 
.
Their Lean development proves the existence of a word within the stated upper bound
for every permutation, together with a matching lower
bound. The authors report Codex assistance with the proof and formalization. As of
Oct. 25, 2026, the public project reported build and axiom checks, but independent
specialist verification had not been reported.
