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 vertices with more than edges contains every tree on vertices. The Lean development proves the benchmark's direct formalization, which states the hypothesis as at least 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. Thomas Bloom, who maintains erdosproblems.com, has since written a proof exposition that he says should contain enough detail to convince anyone following along, and the site now marks the problem proved; 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.
Independent checks
Thomas Bloom (erdosproblems.com exposition): Wrote a proof exposition of the model's argument, describing it as surprisingly simple and elementary and the sketch as detailed enough to convince a reader following along; erdosproblems.com marks the problem proved (Lean). vibemathed separately records that Bloom reviewed the benchmark statement the Lean proof is compared against. · link ↗
The open problem
392272
Nothing mechanically. It records what a problem says, what is known about it, and the standing of any claimed solution.
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.
Disagree with these grades?
Bring a citation: a grade moves on evidence, not on argument.
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.
History of this entry
- CheckedRecorded Thomas Bloom's proof exposition on erdosproblems.com, which now marks the problem proved. No grade moved. source ↗
- CorrectedRecorded the MathDB record for this conjecture as a registration. No grade moved. source ↗
- 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}
}