Papers With

← All papers
First page of Proof of the Erdős-Szemerédi sunflower conjecture

Proof of the Erdős-Szemerédi sunflower conjecture

Matija Bucić, Fankang He, Hyunwoo Lee

math.CO Oct 19, 2026 · v1
formalization combinatorics
Read PDF arXiv abstract
TL;DR
The proof of the Erdős–Szemerédi sunflower conjecture was machine-verified in Lean 4, with the formalization to be released in the Palomar repository.
Abstract
In the 1970s, Erdős and Szemerédi conjectured that for any $n \ge k-1\ge 2$, any collection of subsets of $[n]$ not containing a $k$-sunflower has size at most $c_k^n$ for some $c_k<2$. In the $k=3$ case, this follows from the work of Croot, Lev, and Pach and Ellenberg and Gijswijt on the cap-set problem, through a reduction due to Alon, Shpilka, and Umans. We prove the conjecture for every $k \ge 3$.
Problem

Erdős and Szemerédi conjectured that for every k ≥ 3, any family of subsets of [n] with no k-sunflower has size at most c_k^n for some c_k < 2. Before this work the conjecture was known only for k = 3, via the cap-set results and a reduction due to Alon, Shpilka, and Umans.

Approach

The authors first bound sunflower-free sets in the vector setting [D]^n using the polynomial method. A refined slice-rank-style dimension argument separates one-variable factors lying in a common low-dimensional space of polynomial functions. This gives V_k(D,n) ≤ (C_k·D^{1-1/(k-1)})^n. A probabilistic refinement of the Naslund–Sawin block reduction then transfers the vector bound to set families. The proof was verified in Lean 4.

Results

The conjecture holds for every k ≥ 3: any k-sunflower-free family of subsets of [n] has size at most 3(2 − 1/(16k^3))^n. The formal Lean verification is to be made available in the Palomar repository.