A sunflower is a family of sets whose pairwise intersections are all the same kernel. For positive n and k>=2, let f(n,k) be the least family size forcing a k-sunflower among n-element sets.
This repository contains a six-file Lean development of the classical upper bound, elementary lower constructions, exact small cases, and a product construction for sunflower-free families.
| File | Main content |
|---|---|
Attack01.lean |
Finset sunflower lemma |
Attack02.lean |
Set-family definitions and the Erdős–Rado upper bound |
Attack03.lean |
Lower construction, two-sided bounds, and f(1,k)=k for k>=2 |
Attack04.lean |
Witness lower-bound engine and f(n,2)=2 for n>0 |
Attack05.lean |
Product construction for sunflower-free families |
Attack06.lean |
Two-triangles seed and 6^t < f(2t,3) for t>0 |
The recorded build contains 19 sealed declarations. The finite seed uses kernel decide, not native_decide.
python verification/verify_source.pyThis checks the published source bytes against the pinned manifest. The six Lean hashes match the recorded build receipt in verification/SOURCE-CHECK-2026-09-13.json.
The historical toolchain was leanprover/lean4:v4.31.0-rc1. The original commands and environment are recorded in research/TERMINAL.json.
The full sunflower conjecture is not proved here. The formalization supplies exact classical bounds, reusable constructions, and small-case results; modern upper bounds and the matching upper bound for f(2,3) remain outside this package.
Author: Jared Wilder. License: Apache-2.0.