Finite groups that are the product of every pair of non-conjugate maximal subgroups are soluble
Richie Sater
math.GR
Aug 4, 2026 · v1
TL;DR
The minimal-counterexample structure theorem (unique minimal normal subgroup, faithful conjugation map) is kernel-checked in Lean.
Abstract
We prove that every finite group which coincides with the product of any two of its non-conjugate maximal subgroups is soluble, answering Problem 10.34 of the Kourovka Notebook (V. S. Monakhov, 1986) in the negative. The almost simple case was settled by Tikhonenko and Tyutyanov (2010); the obstacle to the general case was the socle S^k with k >= 2, which no counting bound can control. We remove it with a divisibility criterion: a single pair of automorphism-stable conjugacy classes of subgroups of the simple group S, subject to a valuation inequality, excludes the socle S^k for all k >= 2 and every admissible embedding at once. Such pairs are constructed uniformly for every infinite family of finite simple groups, with Zsigmondy primes as the arithmetic obstruction; the sporadic groups and all remaining small cases are settled by independently re-checkable certificates produced in GAP.
Problem
Kourovka Notebook Problem 10.34 (Monakhov, 1986) asks whether there exists a finite non-soluble group equal to the product of any two of its non-conjugate maximal subgroups. The task is to prove no such group exists.
Approach
A minimal counterexample has a unique minimal normal subgroup S^k embedded in Aut(S) wr S_k. A divisibility (valuation) criterion using a pair of automorphism-stable maximal subgroup classes of the simple group S excludes the socle for all k>=2 and every embedding. Infinite families are handled uniformly via Zsigmondy primes, while sporadic and small cases are settled by GAP certificates. Parts of the structural reduction—quotient inheritance, uniqueness of the minimal normal subgroup, trivial centralizer, and the faithful conjugation map into Aut(N)—are kernel-checked in Lean, with the S^k decomposition checked in Rocq/MathComp.
Results
Every finite group equal to the product of any two non-conjugate maximal subgroups is proved soluble, answering Problem 10.34 in the negative.
