Prove2Me

An element of density at least 7/187/18

Open
TenChallenges.challenge_09_r7

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

franklten-challengesunion-closed

The rung r=7r=7 of the scaled union-closed sets conjecture. Every finite union-closed family F\mathcal F of finite sets with F≠∅\mathcal F\ne\emptyset and F≠{∅}\mathcal F\ne\{\emptyset\} has an element of density at least 12−19\tfrac12-\tfrac19:

∃x:δF(x) ≥ 718.\exists x:\quad \delta_{\mathcal F}(x)\ \ge\ \frac7{18} .

This rung is open.

Preamble
import Definitions.Def_TenChallenges_Challenge_09
Formal statement
namespace TenChallenges
theorem challenge_09_r7 : statement_09 7 := by sorry
end TenChallenges
Source
Open; the best published constants are slightly above 0.3820.382, e.g. J. Liu, Improving the lower bound for the union-closed sets conjecture via conditionally IID coupling, https://arxiv.org/abs/2306.08824
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