The Daykin-Frankl conjecture (Daykin and Frankl 1983) asserts that a family that is an order-convex set 
in the Boolean lattice 
of subsets of an 
-element set has partial
order width at least the same fraction of its size as the partial
order width of 
is of 
. Writing 
for the largest size of an antichain
in 
,
the assertion is
 |
where 
is the floor function. For the whole Boolean
lattice this becomes equality by Sperner's theorem.
For an antichain it is immediate because 
.
Williams (2026) reported a proof, together with the stronger product inequality
 |
The proof was obtained with GPT-5.6 Sol and checked and written up by Williams. Independent external verification had not been reported as of Sep. 7, 2026.
