Erdős Problem 274
If is a group, can there exist an exact covering of by more than one coset of different sizes? (i.e. each element is contained in exactly one of the cosets.)
Mathematical statement
If is a group, can there exist an exact covering of by more than one coset of different sizes? (i.e. each element is contained in exactly one of the cosets.)
The conjectured answer is no: in every such exact covering, two of the subgroups have the same cardinality.
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
erdos_274
theorem erdos_274 : answer(sorry) ↔ ∀ (G : Type*) [Group G], 1 < ENat.card G → ∀ (ι : Type*) [Fintype ι], ∀ (P : Group.ExactCovering G ι), 1 < Fintype.card ι → ∃ i j, i ≠ j ∧ #(P.parts i) = #(P.parts j) := 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