The union-closed sets conjecture states that if 
is a union-closed
set, then an element belongs to at least 
of the sets in 
. Sarvate and Renaud (1989) showed that the conjecture is true
if 
,
where 
is the smallest set in 
, or if 
. They also showed that if the conjecture fails, then
,
where 
is the largest set of 
.
The verified range was successively raised to 18 (Sarvate and Renaud 1990), 24 (Lo Faro 1994a), 27 (Poonen 1992), 32 (Gao and Yu 1998), and 40 (Roberts 1992).
Let 
be the largest universal constant such that every nontrivial finite union-closed
set has an element in at least a fraction 
of its members. The conjecture is equivalent to 
. The Shannon entropy
method of Gilmer (2022) first proved 
, and refinements gave 
(Sawin 2022) and 
(Yu 2023). Liu (2023) reported the computer-assisted
bound 
,
conditional on two numerically verified hypotheses.
Moffat (2026) obtained ceilings for specified classes of single-letter Shannon entropy certificates. If every admissible class contains product laws, the certifiable
constant 
satisfies the first inequality below. If the certificate uses the independent
and identically distributed protocol and its other classes admit component hiding,
it satisfies the second:
 |  |  |
(1)
|
 |  |  |
(2)
|
Here 
is the binary Shannon entropy function. These
are ceilings on those proof methods, not upper bounds on 
.
The first ceiling and the rational weakening 
of the second were formalized in Lean 4. The exact
value 
and a conditional certificate reaching 
were not part of the formalization. Claude agents
found the ceiling results and protocol and carried out most of the computation and
formalization under Moffat's direction. An independent referee checked every quoted
statement and listing against the sources, and all 28 findings from that review were
applied. Independent specialist review of the mathematical argument had not been
reported as of Sep. 13, 2026.
The proof for the case where 
has a 2-set can be effected as follows. Write 
, then partition the sets of 
into four disjoint families 
, 
, 
, and 
, according to whether their intersection with 
is 
, 
, 
, or 
, respectively. It follows that 
by taking unions with 
, where 
is the cardinal number
of 
.
Now compare 
with 
. If 
, then 
, so 
is in at least half the sets of 
. Similarly, if 
, then 
is in at least half the sets (Hoey, pers. comm.).
Unfortunately, this method of proof does not extend to 
, since Sarvate and Renaud show an example of a union-closed
set with 
where none of 
, 
, 
is in half the sets. However, in these cases, there are other
elements which do appear in half the sets, so this is not a counterexample
to the conjecture, but only a limitation to the method of proof given above (Hoey,
pers. comm.).
