Formalize Yu's $0.38234$ bound for the union-closed sets (Frankl) conjecture in Lean 4
Statement
With `A : Finset (Finset n)` and `IsUnionClosed A := ∀ X ∈ A, ∀ Y ∈ A, X ∪ Y ∈ A`, prove (currently a `sorry` in google-deepmind/formal-conjectures): ``` theorem union_closed.variants.yu [Nonempty n] (h_ne_singleton_empty : A ≠ {∅}) (h_union_closed : IsUnionClosed A) : ∃ i : n, (0.38234 : ℚ) * #A ≤ #{x ∈ A | i ∈ x} ``` Meaning: for every finite union-closed family $A\ne\{\emptyset\}$, some element $i$ belongs to at least $0.38234\,|A|$ of the sets in $A$.
Acceptance. SUCCESS: a Lean 4 proof replacing the `sorry` that type-checks against a pinned mathlib toolchain, with `#print axioms <thm>` reported and showing NO `sorryAx` (no remaining gaps). Expected pure-kernel: the only axioms should be `[propext, Classical.choice, Quot.sound]`; state explicitly that this holds. Entropy/real-analytic inequalities are involved; expect pure kernel. PARTIAL: formalize Gilmer's original weaker constant (~0.01), or a finite/small-family variant (`univ_card`, `family_card`) proved in the same file.
Background
Frankl's union-closed sets conjecture (some element lies in at least half the members) is open. J. Gilmer (2022) first proved a positive-constant version via an entropy method; the constant was pushed to $(3-\sqrt5)/2\approx0.38197$ and then to $\approx0.38234$ by L. Yu, *Dimension-free bounds for the union-closed sets conjecture*, Entropy 25(5):767 (2023). Yu's bound is not formalized. Source: formal-conjectures `FormalConjectures/Wikipedia/UnionClosed.lean`, declaration `union_closed.variants.yu`, category `research solved`, body `sorry` (commit 3cc3d454f4).
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | formal-conjectures: UnionClosed.lean (union_closed.variants.yu, sorry) | link |
| REF-02 | Yu, Dimension-free bounds for the union-closed sets conjecture, Entropy 25(5):767 (2023) | link |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.