Erdos-Sos conjecture proved in Lean, in a form marginally weaker than the classical statement
A machine-checked Lean proof establishes the Erdos-Sos conjecture in the benchmark's formalization, which in one parity case assumes one more edge than the classical statement requires.
- Model
- GPT-6 Astra (pre-release)
- Field
- Mathematics
- Date
- 2026-09-03
- Human collaborators
- Tom Adamczewski
- Problem posed
- 1962 · open 64 yrs
Sources
Original work
Independent commentary
What was found
Erdos and Sos conjectured in 1962 that a graph on n vertices with more than (k-1)n/2 edges contains every tree on k+1 vertices. The Lean development proves the benchmark's direct formalization, which states the hypothesis as at least (k-1)n/2 + 1 edges. The proof uses a permutation-word counting argument over ordered host-vertex configurations. It was produced in the same Epoch AI LeanOpenProblems evaluation run as the Koethe disproof, one autonomous attempt per statement, and the compared theorem carries no sorry outside the statement stubs and no axioms beyond the three standard ones.
Novelty check
The conjecture dates to 1962 and is Erdos Problem 548. The weaker statement with (k-2)n edges is an easy induction, and the repository records that the conjecture was previously proved for large k by Ajtai, Komlos, Simonovits and Szemeredi, work that has not appeared in full. The formalized statement is the benchmark's, stated as open in Formal Conjectures at the pinned commit. No prior full formal proof was found in the four registries. The novelty question here is less about priority than about scope, and the scope limit is recorded in the caveats rather than left implicit.
Caveats and known objections
The formalized statement is very slightly weaker than the classical conjecture, and the repository documents the gap precisely rather than glossing it: when (k-1)n is odd, more than (k-1)n/2 edges is already satisfied with one edge fewer than at least (k-1)n/2 + 1 requires, so in that parity case the compared theorem assumes half an edge more. The classical statement implies the formalized one and not conversely. The repository notes that the proof's internal counting lemma derives the sharp classical bound, but only the weaker advertised form is what the comparator compares, so the machine-checked claim is the weaker one and this entry is worded to it. No expert in extremal graph theory is on record as having read it, and the Palomar submission had not landed at entry. Autonomy is autonomous on the same disclosure as the Koethe entry: one attempt, no human seeing or steering the proof search.
Also recorded at
vibemathederdos-problem-548-erdos-sos-conjecture
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Formally verified and Autonomous.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and autonomous for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Erdos-Sos conjecture proved in Lean, in a form marginally weaker than the classical statement. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-09-03-erdos-sos-conjectureBibTeX
@misc{whataifound-openai-2026-conjecture,
title = {Erdos-Sos conjecture proved in Lean, in a form marginally weaker than the classical statement},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by OpenAI / Epoch AI. Verification: Formally verified. Autonomy: Autonomous.},
url = {https://whataifound.org/finding/2026-09-03-erdos-sos-conjecture}
}