Problem CB-002 — the sunflower conjecture

goaldef

Erdős and Rado asked whether some constant C suffices: any family of more than Cᵏ distinct sets of size k must contain three of them meeting in a common core. The best known bound is far from constant in the base.

def goal : Prop :=
  ∃ C : ℕ, ∀ (k : ℕ) (F : Finset (Finset ℕ)),
    (∀ A ∈ F, A.card = k) → C ^ k < F.card →
      ∃ (G : Finset (Finset ℕ)) (core : Finset ℕ),
        G ⊆ F ∧ G.card = 3 ∧ Conjectura.Combinatorics.IsSunflower G core

Builds on

Sunflower

From Mathlib

Data.Finset.Card

import Conjectura.Problems.CB002.Statement · maintainer — open · raw source

Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors

Full credits