Proved on the site (label PROVED at the access of 2026-09-04; page last edited 16 October 2025). The community database lists the status as proved (Lean) as of its last update, dated 2026-09-16, the Lean qualification resting on Collin Yuanjie Ren's formalization of the Frankl–Füredi theorem, which is linked from the Frankl–Füredi claim page (1984). The site records that $T(n,0)=2^{n-1}$ trivially, that Frankl and Füredi [FrFu84b] determined $T(n,r)$ for fixed $r$ and $n$ large in terms of $r$ (the extremal family being the sets of size less than $r$ together with the large sets of Katona's family, in its odd and even forms), that Frankl [Fr77b] had done the case $r=1$ for every $n$, that a yes answer to the second question implies the exponential growth of the chromatic number of the unit-distance graph of $\mathbb R^n$, proved by other means by Frankl and Wilson [FrWi81] (see Problem 704), and that Frankl and Rödl [FrRo87] answered the second question yes.