In September 2026, OpenAI’s GPT-6 Astra produced a proof of the famous Erdős–Sós conjecture, a problem in graph theory that had remained open for more than sixty years (GPT-6 Astra 2026). The proof was formalized in Lean and subsequently simplified by several mathematicians, including Riordan and Scott (Riordan and Scott 2026) and Wood (Wood 2026).
The conjecture is remarkably simple to formulate: how many edges must a graph have to guarantee that it contains every tree of a given size?
Let us recall some definitions. A graph consists of a set of vertices, some pairs of which are joined by edges. A tree is a connected graph without cycles. For example, a path is a tree, and so is a star, in which one central vertex is joined to all other vertices.
Every tree with vertices has exactly edges. However, trees with the same number of vertices can have very different shapes. For example, there are three nonisomorphic trees on five vertices: a path, a star, and a tree with three branches, one of which has length two.
The degree of a vertex is the number of its neighbours. The average degree of a graph is where and denote the sets of vertices and edges, and denotes the number of elements in a finite set . The factor appears because every edge contributes to the degrees of each of its two endpoints.
It is easy to prove that every graph with minimum degree at least contains every tree on vertices. Indeed, start with any vertex of the tree and embed its other vertices one by one, following the edges of the tree. At each step, the required unused neighbour is available because every vertex has at least neighbours.
But what happens if we only know the average degree of the graph?
In 1964, Erdős (Erdős 1964) recorded a conjecture of Erdős and Sós predicting that the average degree only needs to exceed .
For example, the conjecture says that every graph of average degree greater than must contain all three possible trees on five vertices as subgraphs. Here we do not require a tree to be an induced subgraph: extra edges between its chosen vertices may be ignored.
This statement is much stronger than the corresponding assertion for minimum degree. A graph can have many vertices of small degree while still having large average degree, so the simple greedy argument does not work.
The conjecture attracted considerable attention, and many special cases were proved. For example, McLennan (McLennan 2005) established it for all trees of diameter at most four, where the diameter of a tree is the largest distance between two of its vertices. More recently, Pokrovskiy (Pokrovskiy 2024) proved it for sufficiently large trees with bounded maximum degree.
Nevertheless, the general conjecture remained open until 2026.
A graph is called simple if it has no loops or multiple edges.
The theorem is best possible. Indeed, suppose that is divisible by , and consider the disjoint union of copies of the complete graph , in which every pair of distinct vertices is joined by an edge.
Every vertex in this graph has degree , so its average degree is exactly . However, the graph contains no tree on vertices, because each of its connected components has only vertices.
Thus, the strict inequality in the theorem cannot be replaced by a non-strict one.
Equivalently, the theorem says that if a graph with vertices does not contain some fixed tree on vertices, then it has at most edges. This is a sharp result in extremal graph theory, which studies how many edges a graph can have while avoiding a prescribed subgraph.
Let us briefly discuss the proof.
One of its most remarkable features is that it uses a counting argument involving permutations of the vertices. Suppose that has vertices. Consider all possible orderings of its vertices, and in each ordering mark every vertex adjacent to .
How many such marked orderings are there altogether?
If the first vertex is , there are possible orderings of the remaining vertices, and each ordering has exactly possible marks. Therefore, the total number of marked orderings is
The key insight is to relate these marked orderings to embeddings of a prescribed tree.
Every tree with at least two vertices has a leaf, that is, a vertex of degree one. Removing a leaf gives a smaller tree. The proof exploits this simple observation to establish a remarkable counting inequality by induction on the number of vertices of the tree.
The argument uses carefully chosen reversible operations on orderings of graph vertices, including rotations of initial segments and rearrangements of two blocks. These operations allow one to compare the counts associated with a tree and with the smaller tree obtained by removing a leaf.
In particular, if the graph contains no copy of a given tree on vertices, the counting argument shows that Dividing by gives which is exactly the contrapositive of the theorem.
The difficult part is establishing the counting inequality; once that is done, the conclusion follows immediately.
The discovery has the following history. GPT-6 Astra found the argument during experiments with the FrontierMath Erdős benchmark, and its proof was verified in the Lean proof assistant. Riordan and Scott (Riordan and Scott 2026) subsequently presented a shorter and more natural version of the argument. Wood (Wood 2026) and Frederickson (Frederickson 2026) also wrote independent expositions of the central counting ideas.
The result has interesting consequences for Ramsey theory. For example, it implies that if the edges of the complete graph are coloured with colours, then at least one colour class contains every tree on vertices. Indeed, one colour class must have average degree greater than , so the theorem applies to that class.
The Erdős–Sós theorem is a striking example of how a very simple combinatorial statement can resist proof for decades and then yield to an unexpectedly elegant argument. Its final conclusion is sharp: an average degree just greater than already forces every possible tree on vertices, regardless of how irregularly the edges of the graph are distributed.