Vela

erdős #274 · Herzog-Schönheim conjecture

← #273 · #275 (packet.json; erdosproblems.com)

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

Worked, still open.

group theory · open · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239
vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

A coset $gH$ always has the same size as the subgroup $H$. So “different sizes” just means you are using cosets of different subgroups (with different orders).

candidate solution ↗

llm-hunter · gpt 5.2, gpt pro 5.2 · unverified

2 LLM attack(s) recorded (gpt 5.2, gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 20 · open (literature)

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)
formal-conjectures/274.lean ↗

status

open

notary

vela reproduce examples/erdos-problems
  • packet.json · sha256 7bf85956d146135c2f41f83b5e6849accd83de3b8a673f5f42b2b25c3744c090

finding.noted · reviewer:will-blair · 1 day

renders the record as of vev_d199cb2e · 1,338 events · hub

Search Vela

Jump to a section, signal, campaign, document, primitive, work path, frontier, record index, atlas, constellation, agent, capability, or full-state search.