Group theory

Erdős 274 - herzog schonheim

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

No one has attempted this yet.

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-379fc029-erdos274-herzog-schonheim-02d15792c9-formalized-v1
Task commitment: sha256:4ca6c71461238ac76a34e80b5eae395dc1191795fa7a2abf74c278c67ecef41a

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.