---

Claim. The answer to the question of Problem 703 is yes. Theorem 1.1 of Forbidden intersections, recorded with its proof on the library page Theorem 1.1, states that for every $0<\eta<1/4$ there is $\epsilon>0$ such that a family $\mathcal F$ of subsets of an $n$-element set with no two members meeting in exactly $l$ points, where $\eta n<l<(1/2-\eta)n$ is an integer, has at most $(2-\epsilon)^n$ members; the library page checks that the bound also holds under the problem's convention, which forbids the intersection for every pair including $A=B$. In the problem's notation this gives, for every $\epsilon>0$, a $\delta>0$ with $T(n,r)<(2-\delta)^n$ whenever $\epsilon n<r<(1/2-\epsilon)n$: for $\epsilon<1/4$ take $\delta$ below the theorem's constant, and for $\epsilon\ge1/4$ the range of $r$ is empty. The proof deletes coordinates one at a time while tracking a widening forbidden interval of intersection sizes, with Harper's isoperimetric inequality as its external input. The site notes that a yes answer implies the exponential growth of the chromatic number of the unit-distance graph of $\mathbb R^n$, which Frankl and Wilson [FrWi81] had proved by other means.

Depends on. Frankl and Rödl (1987), Theorem 1.1.

Acceptance. Refereed: Trans. Amer. Math. Soc. 300 (1987), no. 1, 259–286, received 24 October 1985; the issue is dated March 1987, and the page is dated to the first day of that month. Reviewed: Thomas Bloom, the site's curator, marks the problem proved and credits the yes answer to Frankl and Rödl [FrRo87]. The library's compilation of the theorem's proof chain is reading coverage and not acceptance evidence.

Formalization. Boris Alexeev's repository holds a Lean 4 development, added on 2026-08-17, whose header calls it a formalization of a solution to the problem, names Frankl and Rödl as the informal authors and "Codex" and "GPT-5.6 Sol" as the formal authors, and cites a write-up tex/703.tex for the mathematical proof and the formalization map. Its top-level theorem states the problem's second question in the problem's own form, for every $\epsilon>0$ a $\delta>0$ with $T(n,r)<(2-\delta)^n$ whenever $\epsilon n<r<(1/2-\epsilon)n$, under the convention that forbids the intersection for every pair including $A=B$, and the Frankl–Rödl argument is carried in a separate module; the file is linked above at the commit the formal-conjectures statement file pins when it names the development as the problem's formal proof. This corpus has not built or audited that development, so the page lists no formalized evidence; the acceptance rests on the refereed paper and the curator's credit.