Erdős problem 548: the Erdős–Sós conjecture

Reference: erdosproblems.com/548

Every graph on n ≥ k + 1 vertices with at least (k - 1) n / 2 + 1 edges contains every tree on k + 1 vertices (erdos_548).

Proof outline

For each permutation word of the host vertices, distinguish its first vertex as a root image. Count the prefixes of its remaining word which end at a neighbour of that root image and support a rooted copy of the target tree.

Two reversible word operations provide the induction:

• Rotating the first qualifying prefix past the rest of a prefix gives the branch-gluing inequality (marked_word_gluing_count).
• Reversing both blocks at a cut moves the root to a newly attached leaf, losing at most one state per full word (rooted_word_leaf_move_count).

Splitting at a nonleaf root, or deleting a leaf root, then proves rooted_word_tree_bound: the number of all adjacency-marked states is at most the rooted-copy count plus (t - 2) * n! for a target of order t ≥ 2. The marked-state count is exactly 2 * |E(G)| * (n - 1)! (full_word_base_count). If the target is absent, cancellation yields 2 * |E(G)| ≤ (t - 2) * n (tree_free_edge_bound), contradicting the stated density. All counts and injections are finite and exact.

theorem Erdos548.full_word_base_count {V : Type u_1} [Finite V] [DecidableEq V] (G : SimpleGraph V) (l₀ : List V) (hl : l₀.Nodup) (hall : ∀ (b : V), b ∈ l₀) : (fullWordCount l₀ G.Adj fun (x : V) (x_1 : Finset V) => True) = (l₀.length - 1).factorial * (2 * G.edgeSet.ncard)

theorem Erdos548.rooted_word_count_zero_of_not_contained {U : Type u_1} {V : Type u_2} [DecidableEq V] (T : SimpleGraph U) (r : U) (G : SimpleGraph V) (h : ¬T.IsContained G) (l₀ : List V) : rootedWordCount T r G l₀ = 0

theorem Erdos548.tree_free_edge_bound {U V : Type} [Fintype U] [Fintype V] (T : SimpleGraph U) (hT : T.IsTree) (ht : 2 ≤ Fintype.card U) (G : SimpleGraph V) (hn : 0 < Fintype.card V) (hfree : ¬T.IsContained G) : 2 * G.edgeSet.ncard ≤ (Fintype.card U - 2) * Fintype.card V

theorem Erdos548.erdos_548 (n k : ℕ) : k + 1 ≤ n → ∀ (G : SimpleGraph (Fin n)), (↑k - 1) / 2 * ↑n + 1 ≤ ↑G.edgeSet.ncard → ∀ (T : SimpleGraph (Fin (k + 1))), T.IsTree → T.IsContained G

Erdős problem #548 (the Erdős–Sós conjecture). 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, as a subgraph (not necessarily induced). This is the statement of the FrontierMath Erdős benchmark, following the phrasing on erdosproblems.com; the classical phrasing "more than $\frac{t-2}{2} n$ edges, trees on $t$ vertices" (with $t = k + 1$) is recovered by Erdos548.tree_free_edge_bound.