Erdős–Sós conjecture: (k-1)n/2 + 1 edges force every tree on k+1 vertices (Erdős #548)

Let $n\geq k+1$. Prove or disprove: every graph on $n$ vertices with at least $\frac{k-1}{2}n+1$ edges contains every tree on $k+1$ vertices (as a subgraph, not necessarily induced). The edge bound would be best possible: a disjoint union of copies of $K_k$ has $\frac{k-1}{2}n$ edges and contains no tree on $k+1$ vertices, since every component has only $k$ vertices.

Acceptance. FULLY RESOLVES: (a) a complete proof of the conjecture for all $n\geq k+1$ — machine-checkable (Lean/Coq) preferred, else a full written proof with all steps (a published, complete proof for all $k\geq k_0$ with an explicit effective threshold $k_0$, combined with proofs covering the finitely many remaining $k<k_0$ — note each such $k$ still requires an argument valid for ALL $n\geq k+1$, so finite computation alone cannot close it — also fully resolves); or (b) a counterexample — explicit $n$, $k$, a graph $G$ on $n$ vertices with at least $\frac{k-1}{2}n+1$ edges (machine-readable), and a specific tree $T$ on $k+1$ vertices, with a machine-checkable certificate that $T$ is not a subgraph of $G$ (exhaustive subgraph-isomorphism search transcript or SAT UNSAT certificate), plus the verification code. ADVANCES: a proof for a natural class of trees or host graphs strictly beyond those stated in the background (e.g. all bounded-degree trees, spiders, or hosts with no $5$-cycle); a general bound $c\,kn$ edges forcing all trees on $k+1$ vertices with $c$ strictly below $1$ (improving the trivial factor stated in the background) by proof; exhaustive certified verification of the conjecture for all $(n,k)$ up to stated limits with reproducible code and exhaustiveness certificates; or a Lean formalisation of the statement plus the Erdős–Gallai path case. Deliver the proof file, the counterexample + certificates + checker, or the verification code and attained range.