Union-closed sets conjecture

Open

TenChallenges.challenge_09

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

franklten-challengesunion-closed

The 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 that lies in at least half of its members:

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

The conjecture is equivalent to the statement $\mathrm{UC}(r)$ for all $r$ of the scaled Challenge 9, since the densities in a fixed finite family take finitely many values. The best known bound is slightly above $0.382$ ; the conjecture is open.

Formalization Note. The type U has decidable equality and may be in any universe; the density is density F x : ℚ, with denominator $\max(1,|\mathcal F|)$ .

Preamble

import Definitions.Def_TenChallenges_Challenge_09

Formal statement

namespace TenChallenges
theorem challenge_09 {U : Type*} [DecidableEq U] (F : Finset (Finset U))
    (hF : IsUnionClosed F) (hne : Nondegenerate F) : ∃ x, density F x ≥ (1 / 2 : ℚ) := by sorry
end TenChallenges

Source

Frankl's union-closed sets conjecture, as stated in H. Bruhn, O. Schaudt, The journey of the union-closed sets conjecture, Graphs Combin. 31 (2015), https://doi.org/10.1007/s00373-014-1515-0, Conjecture 1; equivalent to the universal form of V. Bajpai, N. Bowler, J. Carmesin, U. Okur, 10 Scalable Challenges in Combinatorics, AI4Math @ CICM 2026, challenge 9

Read-back

What the Lean code literally says, in plain math · claude-fable-5-1

The theorem asserts: for every natural number $r \in \{0, 1, 2, \dots\}$ , the proposition $\operatorname{statement}_{09}(r)$ holds. Unfolding that proposition, the full claim is (for an arbitrary, fixed universe of types):

For every $r \in \mathbb{N}$ , for every type $U$ equipped with a decidable equality (a procedure deciding whether two elements of $U$ are equal; $U$ may be finite or infinite and is otherwise unrestricted), and for every finite family $F$ of finite subsets of $U$ (a finite set whose members are finite subsets of $U$ , without repetition): if

$F$ is union-closed, meaning that for all finite subsets $A, B$ of $U$ , $A \in F$ and $B \in F$ imply $A \cup B \in F$ ( $A = B$ allowed; nothing is required about intersections or about $\emptyset$ ), and
$F$ is nondegenerate, meaning $F \neq \emptyset$ and $F \neq \{\emptyset\}$ (literally equivalent to: $F$ has at least one nonempty member; $\emptyset \in F$ is allowed, and $F$ may consist of a single set),

then there exists an element $x \in U$ with

\frac{\bigl|\{\, A \in F : x \in A \,\}\bigr|}{\max(1,\,|F|)} \;\ge\; \frac{1}{2} \;-\; \frac{1}{r + 2},

where $|\cdot|$ counts members, the left-hand side is the rational number obtained from the natural numbers "number of members of $F$ containing $x$ " and $\max(1,|F|)$ (maximum taken among natural numbers), and on the right-hand side $r$ is viewed as a rational.

Details and edge cases:

Under hypothesis 2, $F \neq \emptyset$ , so the left-hand side is exactly the fraction of members of $F$ that contain $x$ , a rational in $[0,1]$ . Since $r + 2 \ge 2$ , no division by zero occurs; the right-hand side equals $\frac{r}{2(r+2)}$ , which is strictly less than $\frac12$ for every $r$ ( $0, \frac16, \frac14, \frac{3}{10}, \dots$ ). The inequality is non-strict ( $\ge$ ).
Order of quantifiers: $r$ is chosen first, then $U$ and $F$ ; the witness $x$ may depend on all three. The theorem is the conjunction, over all $r$ , of the separate statements $\operatorname{statement}_{09}(r)$ ; the bounds $\frac{r}{2(r+2)}$ increase with $r$ and approach $\frac12$ from below, but no single instance asserts the bound $\frac12$ itself.
For $r = 0$ the bound is $0$ , so that instance only demands that $U$ have an element. If $U$ is empty, hypothesis 2 cannot hold (then $F$ is $\emptyset$ or $\{\emptyset\}$ ), so the claim is vacuous for such $U$ ; for nonempty $U$ the hypotheses are satisfiable (e.g. $F = \{\{a\}\}$ ).
Only existence of $x$ is asserted (no uniqueness), and $x$ need not lie in any member of $F$ .
The declaration supplies no proof: its proof is left as an unfilled placeholder.

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