Frankl's conjecture on shattering in antichains

Let $2^{[n]}$ denote the family of all subsets of $[n]$. A family $\mathcal{F}\subseteq 2^{[n]}$ is an antichain if no two members satisfy $F\subseteq F'$.

Frankl's conjecture. Let $k$ be a non-negative integer and $n\geqslant 2k$. If $\mathcal{F}\subseteq 2^{[n]}$ is an antichain with $\mathcal{F}\not\rightarrow(k+1,2^{k+1})$, then

$$|\mathcal{F}|\leqslant\binom{n}{k}.$$

Frankl proved the conjecture for $k\leqslant 2$, and Anstee and Sali proved it for $k=3$; the general case remains open.