erdos_274

Specification

If `G` is a group then can there exist an exact covering of `G` by more than one cosets of different sizes? (i.e. each element is contained in exactly one of the cosets.)

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof

Lean 4 Statement

theorem erdos_274 : answer(sorry) ↔ ∀ᵉ (G : Type*) (h : Group G) (hG : 1 < ENat.card G),
    (∃ (ι : Type*) (_ : Fintype ι) (P : Group.ExactCovering G ι),
      1 < Fintype.card ι ∧ (Set.range P.parts).Pairwise fun A B ↦ #A ≠ #B)

ID: ErdosProblems__274__erdos_274

Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →

Docs

Verification Pipeline

How zero-trust verification works.

Read docs →

Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.