The Erdős–Sós conjecture proved in Lean

On 3 September 2026 Tom Adamczewski of Epoch AI published a Lean proof of the Erdős–Sós conjecture, found by a pre-release GPT-6 Astra on 26 August in an additional, larger-budget attempt of the FrontierMath Erdős benchmark: a graph with more than (k−2)n/2 edges contains every tree on k vertices. The proof passed Lean’s Comparator check; by 18 September three papers had simplified or expounded it.

State of the claim. Claimed: the repository github.com/tadamcz/erdos548, created 3 September 21:48 UTC, and the proof PDF ("A counting proof for Erdős problem 548", GPT-6 Astra) on erdosproblems.com, last modified 3 September 22:20 UTC (the PDF itself was not read); the article by Adamczewski and Bloom (arXiv 2609.25050, 6 September), appendix B.4. Formalised in Lean: by the README, the proof was found "autonomously" by a pre-release GPT-6 Astra in a ReAct-agent configuration with a $1,000 budget (attempt of 26 August, $363, 20.5 hours of working time, one success among several attempts), "no human saw or steered the proof search"; Comparator (Lean FRO) accepts a proof only with the identical statement and only the axioms propext, Quot.sound, Classical.choice, no sorry; one line was changed in moving from Lean 4.27.0 to 4.28.0. The pass did not build the repository. Bloom reviewed the formal statement; it is very slightly weaker than the classical "more than" when (k−1)n is odd, as the README says plainly. The README also says the repository was written by AI assistants at Adamczewski’s direction. Checked by people: Oliver Riordan and Alex Scott (arXiv 2609.15893, 14 September) write that the conjecture "was recently proved by GPT-6 Astra, using a very ingenious and surprising argument", give a simplified version and determine the extremal graphs; David Wood (arXiv 2609.17877, 15 September) expounds the proof; Bryce Frederickson (arXiv 2609.21159, 18 September) gives a simpler proof through random cyclic orderings. No dispute was found in what was read. Content. By the article: for n ≥ k, a graph on n vertices with more than (k−2)n/2 edges contains every tree on k vertices; Erdős and Sós proposed it in 1962. The argument counts pairs (ordering of the vertices, label j) with v1vj an edge: there are 2m(n−1)! of them, and for a fixed tree T at most C(T) + (k−2)n!, where C(T) = 0 if the graph has no copy of T. Dates. Epoch’s page of 1 September (record evt-0405) was later extended with the additional attempts; its number of attempts (4 for problem 548) differs from the article’s v1 (3), so this record takes its numbers from the article. What the record does not claim: that the pass checked the proof, or which person first read it.