Products of permuted sequences in groups

DefinitionKohl's permuted-products statement (Kourovka 18.50)#✓fully proved

The assertion that for all natural numbers \(n\) and \(k\) with \(1 \le k \le n!\) there are a group \(G\) and pairwise distinct elements \(g_1, \dots, g_n \in G\) such that the set \(\lbrace g_{\sigma(1)} g_{\sigma(2)} \cdots g_{\sigma(n)} : \sigma \in S_n \rbrace\) of products obtained by permuting the factors has exactly \(k\) elements.

def permutedProductsTakeEveryCount : Prop :=
  ∀ n k : ℕ, 1 ≤ k → k ≤ n.factorial →
    ∃ (G : Type) (_ : Group G) (g : Fin n → G), Function.Injective g ∧
      (Set.range fun σ : Equiv.Perm (Fin n) => (List.ofFn fun i => g (σ i)).prod).ncard = k

Used by 1

Used byEvery number of distinct permuted products occurs (Kourovka 18.50)

TheoremEvery number of distinct permuted products occurs (Kourovka 18.50)#●ready to prove

For all natural numbers \(n\) and \(k\) with \(1 \le k \le n!\) there are a group \(G\) and pairwise distinct elements \(g_1, \dots, g_n \in G\) such that the set \(\lbrace g_{\sigma(1)} g_{\sigma(2)} \cdots g_{\sigma(n)} : \sigma \in S_n \rbrace\) of products obtained by permuting the factors has exactly \(k\) elements.

The Kourovka Notebook (21st issue) answers 18.50 "Yes, it is true", by an AI-generated solution confirmed by S. Kohl (P. Monticone, 2026); van Doorn, Judin, Monticone and Morrison (2026) give an independent account.

public theorem_wanted permutedProductsTakeEveryCount_holds : permutedProductsTakeEveryCount

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 18.50 (S. Kohl); resolution: P. Monticone, preprint, 2026 (AI solution confirmed by S. Kohl), https://kourovkanotebookorg.wordpress.com/wp-content/uploads/2026/05/18_50.pdf; W. van Doorn, E. Judin, P. Monticone and D. Morrison, On some problems from the Kourovka Notebook, preprint, arXiv:2607.17477 (2026), arXiv:2607.17477 abstract: for every 1 ≤ k ≤ n! there is a group containing n distinct elements whose n! ordered products take exactly k distinct values (found and verified in Lean by the Aristotle agent); the Kourovka Notebook (21st issue) marks 18.50 solved, https://arxiv.org/abs/2607.17477.

Uses 1

Statement usesKohl's permuted-products statement (Kourovka 18.50)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.