Finite groups that are the product of every pair of non-conjugate maximal subgroups are soluble
Richie Sater
math.GR
Aug 4, 2026 · v2
TL;DR
The minimal-counterexample structural reduction (unique minimal normal subgroup, trivial centralizer, faithful conjugation map) is kernel-checked in Lean.
Abstract
We prove that every finite group that is the product of every pair of its non-conjugate maximal subgroups is soluble, answering Problem 10.34 of the Kourovka Notebook (V. S. Monakhov, 1986) in the negative. Tikhonenko and Tyutyanov settled the almost simple case in 2010. What remains is the possibility of a minimal counterexample whose unique minimal normal subgroup is S^k, with S non-abelian simple and k >= 2. Because k is unbounded, no bound depending on a fixed ratio of subgroup orders can handle all such groups. We rule out this possibility with a divisibility criterion: a single pair of automorphism-stable conjugacy classes of subgroups of S, satisfying a valuation inequality, excludes the configuration for every k >= 2 and every admissible embedding. Such pairs are constructed uniformly for every infinite family of finite simple groups, with Zsigmondy primes as the arithmetic obstruction. The sporadic groups and the finitely many exceptional cases are handled by independently checkable GAP certificates.
Problem
Kourovka Notebook Problem 10.34 asks whether a finite group that is the product of every pair of its non-conjugate maximal subgroups must be soluble. The almost simple case was settled in 2010, leaving minimal counterexamples with socle S^k, S non-abelian simple and k>=2.
Approach
A minimal counterexample is reduced to a group with unique minimal normal subgroup N=S^k embedding in Aut(S) wr S_k. For automorphism-stable conjugacy classes of self-normalizing subgroups, normalizers give maximal subgroups whose orders are computed exactly. A prime-valuation divisibility criterion, independent of k, excludes the factorization configuration for all k>=2 using Zsigmondy primes across infinite families. Sporadic and exceptional cases are handled by GAP certificates. Parts of the structural reduction are kernel-checked in Lean (and Rocq/MathComp).
Results
Every finite group that is the product of every pair of non-conjugate maximal subgroups is soluble, answering Problem 10.34 in the negative. The machine base excludes every non-abelian simple group of order at most 1.05e7 and the criterion closes all infinite families.
