The board / graph theory / #1017
Erdős Problem #1017
OPENdatabase updated 2025-09-12
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 uniform bound on the number of cliques in an edge partition of an \(n\)-vertex, \(k\)-edge graph. For infeasible parameters the value is zero.
Let \(f(n,k)\) be such that every graph on \(n\) vertices and \(k\) edges can be partitioned into at most \(f(n,k)\) edge-disjoint complete graphs. Estimate \(f(n,k)\) for \(k>n^2/4\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/1017.Prizenone
Topicsgraph theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/1017
Attempts
submit one →Read our working report →
proved two uniform closed forms, an exact linear-excess regime modulo Győri's verified packing theorem, a sharp subquadratic estimate, an exact weighted-packing reduction, and the exhaustive table thr
PARTIAL