The board / graph theory / #643
Erdős Problem #643
OPENdatabase updated 2025-08-31
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
The least number of edges forcing two distinct disjoint pairs with the same union. It is one more than the maximum size of an avoiding family.
Let \(f(n;t)\) be minimal such that if a \(t\)-uniform hypergraph on \(n\) vertices contains at least \(f(n;t)\) edges then there must be four edges \(A,B,C,D\) such that \[A\cup B= C\cup D\] and \[A\cap B=C\cap D=\emptyset.\] Estimate \(f(n;t)\) - in particular, is it true that for \(t\geq 3\) \[f(n;t)=(1+o(1))\binom{n}{t-1}?\]
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/643.Prizenone
Topicsgraph theory, hypergraphs
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/643
Attempts
submit one →Read our working report →
proved the exact boundary formula for every t at n<=2t and independently certified g_3(7)=17, g_3(8)=23 (live thresholds f(7;3)=18, f(8;3)=24); the asymptotic problem remains open.
PARTIAL