Papers With

← All papers
First page of The Herzog–Schönheim Conjecture for Solvable Groups

The Herzog–Schönheim Conjecture for Solvable Groups

Murali Menon

math.GR Nov 7, 2026 · v1 math.CO
formalization mathlib algebra
Read PDF arXiv abstract Code
TL;DR
The full proof of the Herzog–Schönheim conjecture for solvable groups is formalized in Lean 4 with Mathlib, with a public repository and axiom check.
Abstract
The Herzog–Schönheim conjecture states that if a group is partitioned into finitely many, and at least two, cosets of subgroups, then two of these subgroups have the same index. We prove the conjecture for all solvable groups, finite or infinite. Sun's bound on unions of cosets, applied in a quotient, is combined with divisibility restrictions on local indices relative to the subgroup generated by the $p$-elements, where $p$ is the largest prime divisor of the order of a minimal counterexample. These restrictions are obtained by counting fixed points in a primitive solvable quotient. This suffices except at the prime $7$, where the counting bound narrowly fails and an additional overlap argument is needed. The proof has been formalized in Lean 4 with mathlib.
Problem

The Herzog–Schönheim conjecture states that any partition of a group into finitely many (at least two) cosets of subgroups contains two subgroups of equal index. It was known only for special classes such as finite nilpotent, pyramidal, simple and symmetric groups.

Approach

The proof reduces to a minimal finite solvable counterexample and takes F to be the subgroup generated by the p-elements, where p is the largest prime divisor of the group order. Sun's bound on unions of cosets is applied in the quotient G/F. It is combined with cyclotomic divisibility restrictions on local indices, obtained by counting fixed points in a primitive solvable quotient. The prime 7 requires an extra overlap argument. The whole proof, including Sun's bound and the finite numerical inequalities, is formalized in Lean 4 with Mathlib, against a statement taken from the Formal Conjectures repository.

Results

The conjecture holds for all solvable groups, finite or infinite. The Lean theorem Erdos274.herzog_schonheim.variants.solvable depends only on the standard axioms propext, Classical.choice and Quot.sound, so it contains no sorry.