The board / graph theory / #548
Erdős Problem #548
PROVED LEANdatabase updated 2026-09-03
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).
Let \(n\geq k+1\). Every graph on \(n\) vertices with at least \(\frac{k-1}{2}n+1\) edges contains every tree on \(k+1\) vertices.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved. The authoritative wording is on erdosproblems.com/548.Prizenone
Topicsgraph theory
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/548
Attempts
submit one →Read our working report →
Exact same-order extremal numbers are proved for every tree (and independently checked for all 106 ten-vertex trees); page \(k=9\) is reduced to 41 tree types and critical hosts with \(n\ge15\), \(e=4
PARTIAL