VibeMathedMath problems solved with AI
Sign in

Erdős Problem #548: the Erdős–Sós conjecture

Erdős problem #548 · erdosproblems.com/548

Let n≥k+1n\ge k+1. Every graph GG on nn vertices with∣E(G)∣≥k−12n+1 |E(G)|\ge \frac{k-1}{2}n+1 contains every tree on k+1k+1 vertices as a not necessarily induced subgraph.

Result
Proved(see note)
Status
Resolved
AI contribution
AI-discovered
Method
Argument
Field
Graph theory
Posed by
Paul Erdős and Vera T. Sós
Year posed
1962
Years open
64y
Solved
2026-08-26
Model
GPT-6 Astra (pre-release)
Vendor
OpenAI
Collaborators
Tom Adamczewski
Verification
Lean-verified
Publication
Announced
Significance
58 / 100
Disclosed cost
$363
Wikipedia
No dedicated article

What was actually shown

For every n,kn,k with k+1≤nk+1\le n, every simple graph GG on nn vertices satisfying∣E(G)∣≥k−12n+1 |E(G)|\ge \frac{k-1}{2}n+1 contains every tree on k+1k+1 vertices.

The proof counts pairs (π,j)(\pi,j) where π=(v1,…,vn)\pi=(v_1,\ldots,v_n) is an ordering of the host vertices and v1vjv_1v_j is an edge. There are exactly2∣E(G)∣(n−1)! 2|E(G)|(n-1)! such pairs. An induction on the target tree bounds this quantity by a rooted-copy count plus(k−1)n!. (k-1)n!. If the target tree is absent, the rooted-copy term vanishes and one obtains2∣E(G)∣≤(k−1)n, 2|E(G)|\le (k-1)n, contradicting the density hypothesis.

What the AI did

A pre-release GPT-6 Astra autonomously found the proof and wrote the Lean formalization in the FrontierMath Erdős benchmark, with no human seeing or steering the proof search. The proof uses a permutation-word counting argument: it counts ordered host-vertex configurations whose first vertex is adjacent to a later vertex, then uses two reversible word operations and induction on the target tree. If the tree is absent, the counting inequality yields2∣E(G)∣≤(k−1)n, 2|E(G)|\le (k-1)n, contradicting the assumed edge density.

Verification

Lean-verified. Checked here on 6 September 2026 from a clone of tadamcz/erdos548 at 3766491: 1,311 lines of Lean, zero sorry outside the statement stubs, zero axiom declarations, no native_decide, unsafe or implemented_by; Comparator configuration present and CI runs it with only propext, Quot.sound and Classical.choice. The statement was autoformalized for the FrontierMath Erdős benchmark and reviewed by Thomas Bloom, and Challenge.lean is copied from that file; it follows erdosproblems.com's phrasing, which differs from the classical one by requiring one extra edge when (t-2)n is odd, a parity margin the repository's README discusses and the internal counting lemma closes. erdosproblems.com, the field's own record, marks the problem PROVED (LEAN) with a proof exposition by Thomas Bloom, which is why this is Resolved rather than Candidate: the canonical tracker has accepted it.

Sources

Submitted by VibeGene on

Changelog2 changes

Discussion