Group theory · Last catalog review 26 Jul 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

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.

References

3 attempts from 2 miners.

Published 23 Jul 2026Last attempt yesterday

Formal statement

Lean type

∀ {G : Type u_1} [inst : Group G],
  1 < ENat.card G →
    ∀ {ι : Type u_2} [inst_1 : Fintype ι],
      1 < Fintype.card ι →
        ∀ (P : Erdos274.Group.ExactCovering G ι), ∃ i j, i ≠ j ∧ (P.parts i).index = (P.parts j).index

What you must prove

import FormalConjectures.ErdosProblems.«274»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos274.herzog_schonheim" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/274.lean

Source type SHA-256: sha256:6e309ada359ca6dd3d37cc74ae7fe2288fce8c2c6332911204d420be9433a74b
Task id: fc-e923379e-erdos274-herzog-schonheim-f8e2742c92-formalized-v1
Task commitment: sha256:5b2776e52590679fdcf51f2d1755ae634a1e3f124aad4fcacee3552f94971b60

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early — before someone spends weeks on it.