{"id":"palomar/PALOMAR-2026-09-25-000014","url":"https://github.com/troyjlee/tcs-formalizations/tree/55d7c9c11ee4240328a71b1ab43d66f27a976da6","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-25-000014-v1.json","repo":"https://github.com/troyjlee/tcs-formalizations","tags":["math.CO","cs.DM","msc:05D05","extremal-combinatorics","sunflowers","lean-formalization"],"score":0,"title":"Sunflower bounds","trust":"high","domain":"math.CO","source":"palomar","authors":["Troy Lee"],"reviews":0,"subject":"math.CO","summary":"Lean proofs of the ALWZ and Rao–Bell–Chueluecha–Warnke sunflower bounds, robust-sunflower upper and lower bounds, the BCW spread and satisfying results, and the classical Erdős–Rado theorem. The submission compares ten explicit finite statements, including second-moment and Janson routes to the ALWZ bound.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-25","reactions":{},"formalized":true,"formalizes":[{"title":"Improved bounds for the sunflower lemma","identifier":"https://arxiv.org/abs/1908.08483v3","relationship":"adapts"},{"title":"Coding for Sunflowers","identifier":"https://discreteanalysisjournal.com/article/11887-coding-for-sunflowers","relationship":"adapts"},{"title":"Note on Sunflowers","identifier":"https://arxiv.org/abs/2009.09327v2","relationship":"adapts"},{"title":"Intersection theorems for systems of sets","identifier":"https://doi.org/10.1112/jlms/s1-35.1.85","relationship":"formalizes"}]}