Erdős–Sós Conjecture
A graph is a set of dots, called vertices, joined by lines, called edges. The degree of a vertex is the number of edges at it. The average degree of a graph is the average of these numbers. A graph with vertices and edges has average degree , because each edge touches two vertices.
A tree is a graph in one piece with no closed loops. With 4 vertices there are two trees: four vertices in a line, and one center with three edges. With 5 vertices there are three trees. A graph contains a tree if you can find the shape of that tree among its edges. All other edges and vertices do not matter.
The question is how many edges force a given tree to appear. Here is a lower limit. Take vertices and join every pair. Each vertex has degree , so the average degree is . This graph has too few vertices for any tree with vertices.
The Erdős–Sós conjecture says that this limit is exact. It says that every graph with average degree above contains every tree with vertices. For , a graph with average degree above 3 must contain all three trees with 5 vertices.
The case is easy to check. An average above 1 means that some vertex has degree at least 2. This vertex and two of its neighbors form the only tree with 3 vertices.
The difficulty for larger is the word "average". Growing a tree is easy when every vertex has a high degree. Place one vertex, then attach the others one at a time. If every vertex has degree at least , a free neighbor is always available, because the tree uses fewer than other vertices.
An average can hide vertices with a low degree. Take one center joined to 100 other vertices. The center has degree 100, the others have degree 1, and the average is just below 2. This graph holds large stars, but it has no line of 4 vertices. So a high degree at a few vertices does not help with every tree.
The easy method first removes vertices with a low degree, until every remaining vertex has degree at least . This is only certain to work when the average degree is at least , about twice the conjectured amount. The conjecture says that half of that average is enough, for all graphs and all trees.
David Wood's exposition reports a proof that GPT-6 Astra found for the FrontierMath Erdős project. The proof is a short counting argument. A formal copy passes Lean, a computer program that checks each step of a proof.