The board / combinatorics / #703
Erdős Problem #703
PROVED LEANdatabase updated 2026-09-16
The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
`T n r` is maximal such that there exists a family \(\mathcal{F}\) of subsets of \(\{1,\ldots,n\}\) of size `T n r` such that \(\lvert A\cap B\rvert\neq r\) for all \(A,B\in \mathcal{F}\) (including \(A=B\)).
Let \(r\geq 1\) and define \(T(n,r)\) to be maximal such that there exists a family \(\mathcal{F}\) of subsets of \(\{1,\ldots,n\}\) of size \(T(n,r)\) such that \(\lvert A\cap B\rvert\neq r\) for all \(A,B\in \mathcal{F}\). Estimate \(T(n,r)\) for \(r\geq 2\). In particular, is it true that for every \(\epsilon>0\) there exists \(\delta>0\) such that for all \(\epsilon n<r<(1/2-\epsilon) n\) we have \[T(n,r)<(2-\delta)^n?\] The answer is yes, proved by Frankl and Rödl [FrRo87].
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/703.Prize$250
Topicscombinatorics
Statement in LeanFormal Conjectures
Solution in Leanyes
OEISA390645
Original pageerdosproblems.com/703
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.