Source labels openChecked July 26, 2026

Erdős Problem 274

Let $G$ be a group, and let $A = \{a_1G_1, \dots, a_kG_k\}$ be a finite system of left cosets of subgroups $G_1, \dots, G_k$ of $G$ .

Group theory AMS 20

Mathematical statement

Let $G$ be a group, and let $A = \{a_1G_1, \dots, a_kG_k\}$ be a finite system of left cosets of subgroups $G_1, \dots, G_k$ of $G$ .

Herzog and Schönheim conjectured that if $A$ forms a partition of $G$ with $k > 1$ , then the indices $[G:G_1], \dots, [G:G_k]$ cannot be distinct.

Statement source: Erdős Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

herzog_schonheim

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem herzog_schonheim {G : Type*} [Group G] (hG : 1 < ENat.card G) {ι : Type*} [Fintype ι]    (hι : 1 < Fintype.card ι) (P : Group.ExactCovering G ι) :    ∃ i j, i ≠ j ∧ (P.parts i).index = (P.parts j).index := by  sorry

Statement source: Formal Conjectures
Lean version: v4.27.0
Placeholder: Present; no proof artifact
Source evidence: Pinned source index
Fidelity review: Community formulation

References

Pinned Formal Conjectures sourceformalization erdosproblems.com/274background Wikipediabackground arXiv:1803.08301background