An element of density at least $3/8$

Open

TenChallenges.challenge_09_r6

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

franklten-challengesunion-closed

The rung $r=6$ 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-\tfrac18$ :

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

Preamble

import Definitions.Def_TenChallenges_Challenge_09

Formal statement

namespace TenChallenges
theorem challenge_09_r6 : statement_09 6 := by sorry
end TenChallenges

Source

Z. Chase, S. Lovett, Approximate union closed conjecture, https://arxiv.org/abs/2211.11689, Theorem 1 (density at least

\frac{3-\sqrt5}{2}

); independently 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 3/83/83/8

An element of density at least $3/8$