The board / graph theory / #719
Erdős Problem #719
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).
Let \(r\geq 2\), and let \(\mathrm{ex}_r(n;K_{r+1}^r)\) be the maximum number of \(r\)-edges that can be placed on \(n\) vertices without forming a \(K_{r+1}^r\) (the \(r\)-uniform complete graph on \(r+1\) vertices). Is every \(r\)-hypergraph \(G\) on \(n\) vertices the union of at most \(\mathrm{ex}_{r}(n;K_{r+1}^r)\) many copies of \(K_r^r\) and \(K_{r+1}^r\), no two of which share a \(K_r^r\)?
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open. The authoritative wording is on erdosproblems.com/719.Prizenone
Topicsgraph theory, hypergraphs
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/719
Attempts
submit one →Read our working report →
For the intended range r>=2, proved the conjecture uniformly for n<=r+3 and exactly for (r,n)=(3,7), with a standalone exhaustive checker; the general covering-design inequality (7) remains open.
PARTIAL