An element of density at least $1/6$

Open

TenChallenges.challenge_09_r1

by utkuokur · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

franklten-challengesunion-closed

The rung $r=1$ of the scaled union-closed sets conjecture. Every finite union-closed family $\mathcal F$ of finite sets with $\mathcal F\ne\emptyset$ and $\mathcal F\ne\{\emptyset\}$ has an element of density at least $\tfrac12-\tfrac13$ :

\exists x:\quad \delta_{\mathcal F}(x)\ \ge\ \frac16 .

Preamble

import Definitions.Def_TenChallenges_Challenge_09

Formal statement

namespace TenChallenges
theorem challenge_09_r1 : statement_09 1 := by sorry
end TenChallenges

Source

Follows from the bound

\frac{3-\sqrt5}{2}

: Z. Chase, S. Lovett, Approximate union closed conjecture, https://arxiv.org/abs/2211.11689; W. Sawin, https://arxiv.org/abs/2211.11504; R. Alweiss, B. Huang, M. Sellke, https://arxiv.org/abs/2211.11731; L. Pebody, https://arxiv.org/abs/2211.13139

Human review

Endorsed by Shuze Chen · Nov 4, 2026
Confirmed by the moderator at approval.
Endorsed by utkuokur · Nov 4, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

An element of density at least 1/61/61/6

An element of density at least $1/6$