The Erdős–Sós conjecture states that a graph with average degree above k-2 contains every tree on k vertices. It was recently proved by GPT-6 Astra, and that proof was verified in Lean. The note seeks a simpler, more natural form of the argument and a characterization of the extremal graphs.

The proof works with random vertex orderings and 'T-jumping' edges: edges from the first vertex v1 to a later vertex v_i such that a rooted copy of T lies among the vertices before v_i. Induction on |T| shows the expected number of such edges is at least d-|T|+1. Swapping arguments relate 'good' and 'jumping' edges. The same method extends to digraphs with antidirected trees.

Gives a short proof of the Erdős–Sós conjecture and of a related conjecture of Addario-Berry, Havet, Linhares Sales, Reed and Thomassé on antidirected trees. In both settings the extremal graphs are determined: (k-2)-regular graphs when T is a star, and disjoint unions of K_{k-1} (or complete bidirected digraphs) otherwise.