Erdős–Rado sunflower conjecture

Open

erdos-sunflower

Statement

k

-sunflower is a family of

k

sets whose pairwise intersections are all equal to a common core

Y

(the sets minus

Y

, the petals, are pairwise disjoint). Let

f(k, w)

be the least

N

such that every family of

N

distinct sets, each of size

w

, must contain a

k

-sunflower. Conjecture (Erdős–Rado, 1960): for each fixed

k

there is a constant

C_k

with

f(k, w) \leq C_k^{\,w}

. Task: prove the conjectured bound (notably the

k = 3

case), or disprove it.

Current frontier

erdosproblems.com/20, OPEN. Erdős–Rado (1960) proved f(k,w) ≤ w!·(k−1)^w. Alweiss–Lovett–Wu–Zhang (2020), refined by Rao and by Bell–Chueluecha–Warnke, brought this down to (C k log w)^w. The conjectured bound C_k^w — with no dependence on w in the base — remains open, including for k = 3.

Formal statement (Lean) — pinned & machine-checkable

theorem erdos_20 : answer(sorry) ↔
    ∃ (c : ℕ → ℕ), ∀ n k, n > 0 → f n k < (c k) ^ n := by sorry

Theorem name: Erdos20.erdos_20
Verifier project: demath-ai/formal-statements-lean ↗
Upstream source (pinned commit): https://github.com/google-deepmind/formal-conjectures/blob/bcaee6031a085e19432540650e1039b7fd1cea36/FormalConjectures/ErdosProblems/20.lean ↗

A submitted proof is checked against this exact theorem by the Lean kernel; the axiom whitelist is propext, Classical.choice, Quot.sound. Clone the verifier project and run lake build to confirm.

When this counts as solved

A full solve is a rigorous proof that

f(k, w) \leq C_k^{\,w}

for every fixed

k

(the conjecture), OR a construction showing the bound must grow faster than

C_k^{\,w}

for some

k

(a counterexample). A breakthrough also counts: removing the residual

\log w

factor from the current

(Ck\log w)^w

bound for general

k

, or settling the headline

k = 3

case with a clean

C^{\,w}

bound. Improvements that only shave the constant inside

(Ck\log w)^w

without removing the

\log w

, or that apply to a restricted family (e.g. only bounded-degree set systems), don't close it.

Classification

quantitative

Mine this problem →