Exact directed L/X diameter of the symmetric group
For , let be the diameter of the directed Cayley graph of generated by the left cyclic shift and the transposition , without inverses: the least such that every permutation is a product of at most factors, each or . Glushkov (1968) asked for . Chervov, Fedoriaka et al. (2025) conjectured for odd and for even . Is that true?
- Result
- Proved(see note)
- Status
- Resolved
- AI contribution
- AI-assisted
- Method
- Argument
- Field
- Cayley graphs, permutation groups, directed diameter
- Posed by
- V. M. Glushkov (1968, Kibernetika 4(2)) asked for the diameter; the formula was conjectured by Chervov, Fedoriaka et al., CayleyPy Growth, arXiv:2509.19162 (2025)
- Year posed
- 1968
- Years open
- 58y
- Solved
- 2026-10-19
- Model
- OpenAI Codex (Astra, per the submitter)
- Vendor
- OpenAI
- Collaborators
- S. Uskov, A. Chervov, F. Levkovich-Maslyuk, I. Litvak, A. Smolensky
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Significance
- 12 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
The theorem LX.exact_diameter_all establishes the stated diameter formula for every n ≥ 5, with matching upper and lower bounds. LX.sharp_route_all proves the existence of an L/X word within the sharp bound between any ordered pair of permutations. The result concerns the directed two-generator problem, OEIS A039745. The formalization does not provide an executable shortest-word solver.
What the AI did
Astra, used through OpenAI Codex, assisted with proof development, auxiliary lemmas, Lean 4 formalization, and debugging.
Verification
Read by this site on 3 November 2026, not rebuilt here. Release v1.0.0 (commit 9e04062, Lean 4.34.0, Mathlib v4.34.0, 310 modules): no sorry, admit, axiom declarations, native_decide, unsafe, opaque or implemented_by. The headline statement was read with its definitions: states are Equiv.Perm (Fin n), L is finRotate n, X is swap 0 1, a word evaluates to the product of its letters, length is the least word length reaching a permutation, and diameter is the maximum length; LX.diameter_eq_max_dist identifies it with the maximum directed distance over ordered pairs. LX.exact_diameter_all states the formula over the rationals for all n >= 5 with no extra hypothesis. The GitHub Actions run on that commit (40743009401, 28 October) built 9,235 jobs and the shipped audit printed PASS for 4,593 project theorems, axioms only propext, Classical.choice and Quot.sound. A separate breadth-first search written here gave diameters 11, 18, 25, 35, 45, 58 for n = 5 to 10, matching the formula (which fails at n = 3, 4, as the bound n >= 5 expects). No independent expert has reviewed the proof, and the statement audit is this site's alone.
Sources
Submitted by Sergei Uskov on