Sunflower lemma

DefinitionFamilies containing a sunflower#✓fully proved

Let \(n\) and \(k\) be natural numbers. A family \(F\) of subsets of \(\{0, \dots, n-1\}\) contains a \(k\)-sunflower if some subfamily \(T \subseteq F\) with exactly \(k\) members satisfies \(A \cap B = C \cap D\) for all \(A, B, C, D \in T\) with \(A \ne B\) and \(C \ne D\), that is, all pairwise intersections of distinct members of \(T\) are equal.

def ContainsKSunflower {n : ℕ} (k : ℕ) (F : Finset (Finset (Fin n))) : Prop :=
  ∃ (T : Finset (Finset (Fin n))), T ⊆ F ∧ T.card = k ∧
    ∀ ⦃a⦄, a ∈ T → ∀ ⦃b⦄, b ∈ T → a ≠ b → ∀ ⦃c⦄, c ∈ T → ∀ ⦃d⦄, d ∈ T → c ≠ d → a ∩ b = c ∩ d

Used by 1

Used bySunflower-free families

DefinitionSunflower-free families#✓fully proved

Let \(n\) and \(k\) be natural numbers. A family \(F\) of subsets of \(\{0, \dots, n-1\}\) is \(k\)-sunflower-free if it does not contain a \(k\)-sunflower.

def IsKSunflowerFree {n : ℕ} (k : ℕ) (F : Finset (Finset (Fin n))) : Prop :=
  ¬ ContainsKSunflower (n := n) k F

Uses 1 · Used by 1

Statement usesFamilies containing a sunflower

Used byErdős–Szemerédi sunflower conjecture for \(k \ge 4\)

DefinitionErdős–Szemerédi sunflower conjecture for \(k \ge 4\)#✓fully proved

The proposition asserts that for every natural number \(k \ge 4\) there is a real number \(c\) with \(0 < c < 2\) such that, for all sufficiently large \(n\), every \(k\)-sunflower-free family of subsets of \(\{0, \dots, n-1\}\) has at most \(c^n\) members.

The bound is required only for large \(n\) because for \(2^n < k\) the family of all subsets of \(\{0, \dots, n-1\}\) is \(k\)-sunflower-free. The case \(k = 3\), proved by Naslund and Sawin, is omitted.

def conjecture : Prop :=
  ∀ k : ℕ, 4 ≤ k →
    ∃ c : ℝ, 0 < c ∧ c < 2 ∧
      ∀ᶠ n : ℕ in Filter.atTop,
        ∀ F : Finset (Finset (Fin n)),
          IsKSunflowerFree k F →
            (F.card : ℝ) ≤ c ^ n

Uses 1 · Used by 1

Statement usesSunflower-free families

Used byThe Erdős–Szemerédi sunflower bound for \(k \ge 4\)

TheoremThe Erdős–Szemerédi sunflower bound for \(k \ge 4\)#●ready to prove

For every natural number \(k \ge 4\) there is a real number \(c\) with \(0 < c < 2\) such that, for all sufficiently large \(n\), every family of subsets of \(\{0, \dots, n-1\}\) that contains no \(k\)-sunflower has at most \(c^n\) members. Here a \(k\)-sunflower in a family is a choice of \(k\) distinct members whose pairwise intersections are all equal.

Resolved true: Proved: Bucić, He and Lee (arXiv:2610.26686, 2026, Theorem 1) show that for every k >= 3 and n >= 1 a family of subsets of [n] with no k-sunflower has at most 3(2 - 1/(16k^3))^n members, which gives the formalized bound c^n with c < 2 for each k >= 4 and all large n. erdosproblems.com/857 (checked 2026-10-22) records this bound as known. The paper states that the proof of its vector-sunflower bound (Theorem 2) was found by ChatGPT 6 Astra Pro and verified by the authors. Source: Matija Bucić, Fankang He and Hyunwoo Lee, Proof of the Erdős-Szemerédi sunflower conjecture, arXiv:2610.26686 (2026), https://arxiv.org/abs/2610.26686; T. F. Bloom, Erdős Problem #857, erdosproblems.com, https://www.erdosproblems.com/857. Moved from OpenConjectures/Combinatorics/ErdosProblem857WeakSunflower.

public theorem_wanted conjecture_holds : conjecture

Uses 1

Statement usesErdős–Szemerédi sunflower conjecture for \(k \ge 4\)

DefinitionSunflower#✓fully proved

Let \(r \in \mathbb{N}\) and let \(S\) be a family of subsets of a type \(X\). Then \(S\) is an \(r\)-sunflower if \(S\) has exactly \(r\) members (its cardinality is taken to be \(0\) when \(S\) is infinite) and any two distinct members \(A \ne B\) of \(S\) satisfy \(A \cap B = \bigcap S\), the intersection of all members of \(S\).

def IsSunflower (r : ℕ) (S : Set (Set X)) : Prop :=
  S.ncard = r ∧ S.Pairwise (fun A B ↦ A ∩ B = ⋂₀ S)

Sources

• R. Alweiss, S. Lovett, K. Wu, and J. Zhang, Improved bounds for the sunflower lemma, Annals of Math 194 (3), 2021, Definition 1.1.

Used by 1

Used byAlweiss–Lovett–Wu–Zhang sunflower bound

DefinitionBounded-size set systems#✓fully proved

Let \(w \in \mathbb{N}\) and let \(\mathcal{F}\) be a family of subsets of a type \(X\). Then \(\mathcal{F}\) is a \(w\)-set system if every member \(A \in \mathcal{F}\) has at most \(w\) elements, where the size of an infinite set is taken to be \(0\).

def IsSystem (w : ℕ) (ℱ : Set (Set X)) : Prop := ∀ A ∈ ℱ, A.ncard ≤ w

Sources

• R. Alweiss, S. Lovett, K. Wu, and J. Zhang, Improved bounds for the sunflower lemma, Annals of Math 194 (3), 2021, second sentence of the introduction.

Used by 1

Used byAlweiss–Lovett–Wu–Zhang sunflower bound

DefinitionSunflower lower bound#✓fully proved

For natural numbers \(r\) and \(w\) and a real number \(C\), the lower bound is the real number

\[\left(C\, r^3 \log_{1.9} w \, \log_{1.9}(\log_{1.9} w)\right)^w,\]

where \(\log_{1.9} x = \ln x / \ln 1.9\), with the convention \(\ln 0 = 0\).

Following the authors, logarithms are taken to base \(1.9\); see the paragraph directly after Theorem 1.4 of Alweiss, Lovett, Wu, and Zhang, Improved bounds for the sunflower lemma.

noncomputable def lowerBound (r : ℕ) (C : ℝ) (w : ℕ) : ℝ :=
  (C * r ^ 3 * logb 1.9 w * logb 1.9 (logb 1.9 w)) ^ w

Used by 1

Used byAlweiss–Lovett–Wu–Zhang sunflower bound

DefinitionSunflower constant#●ready to state

An unspecified real number \(C\), the absolute constant in the Alweiss–Lovett–Wu–Zhang sunflower bound (Theorem 1.4); it does not depend on \(r\) or \(w\).

public def_wanted C : ℝ

Sources

• R. Alweiss, S. Lovett, K. Wu, and J. Zhang, Improved bounds for the sunflower lemma, Annals of Math, 194 (3) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_improved_bounds_sunflower_lemma of the lean-eval benchmark.

Used by 1

Used byAlweiss–Lovett–Wu–Zhang sunflower bound

TheoremAlweiss–Lovett–Wu–Zhang sunflower bound#●statement formalized

Let \(C\) be the sunflower constant, a real number not depending on \(r\) or \(w\). Let \(r \ge 3\) and \(w \ge 2\) be natural numbers, let \(X\) be a finite type, and let \(\mathcal{F}\) be a \(w\)-set system of subsets of \(X\), that is, every member of \(\mathcal{F}\) has at most \(w\) elements. If \(\mathcal{F}\) has at least

\[\left(C\, r^3 \log_{1.9} w \, \log_{1.9}(\log_{1.9} w)\right)^w\]

members, then some subfamily \(S \subseteq \mathcal{F}\) is an \(r\)-sunflower: \(S\) has exactly \(r\) members and any two distinct members of \(S\) intersect in \(\bigcap S\).

This is Theorem 1.4 (main theorem, sunflowers); logarithms are to base \(1.9\), as in the paper. We require \(w \ge 2\), as the paper assumes \(\log \log w > 0\).

public theorem_wanted theorem_1_4 (r : ℕ) (hr : r ≥ 3) (X : Type*) [Finite X] (ℱ : Set (Set X)) (w : ℕ)
      (hw : w ≥ 2) (hℱ₁ : Set.IsSystem w ℱ) :
      ℱ.ncard ≥ lowerBound r ❰C❱ w → ∃ S ⊆ ℱ, Set.IsSunflower r S

Sources

• R. Alweiss, S. Lovett, K. Wu, and J. Zhang, Improved bounds for the sunflower lemma, Annals of Math, 194 (3) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_improved_bounds_sunflower_lemma of the lean-eval benchmark.

Uses 4

Statement usesSunflower constant · Sunflower lower bound · Sunflower · Bounded-size set systems

6 fully proved1 ready to prove1 statement formalized1 ready to state

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.