Problem CB-002 — the sunflower conjecture

Conjectura.Problems.CB002.Statement

/-
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
-/
import Conjectura.Defs.Mathematics.Combinatorics.Sunflower
import Mathlib.Data.Finset.Card

/-! # Problem CB-002 — the sunflower conjecture

LOCKED: solvers cannot modify this file.
-/

namespace Conjectura.CB002

/-- 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

end Conjectura.CB002