VibeMathed reports this item as resolved. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Precise statement
Let $n\ge k+1$. Every graph $G$ on $n$ vertices with
$$
|E(G)|\ge \frac{k-1}{2}n+1
$$
contains every tree on $k+1$ vertices as a not necessarily induced subgraph.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement
fidelity, correctness, priority, or novelty.
What AI did
GPT-6 Astra (pre-release)
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 yields
$$
2|E(G)|\le (k-1)n,
$$
contradicting the assumed edge density.
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.
For every $n,k$ with $k+1\le n$, every simple graph $G$ on $n$ vertices satisfying
$$
|E(G)|\ge \frac{k-1}{2}n+1
$$
contains every tree on $k+1$ vertices.
The proof counts pairs $(\pi,j)$ where $\pi=(v_1,\ldots,v_n)$ is an ordering of the host vertices and $v_1v_j$ is an edge. There are exactly
$$
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!.
$$
If the target tree is absent, the rooted-copy term vanishes and one obtains
$$
2|E(G)|\le (k-1)n,
$$
contradicting the density hypothesis.
Known method families
argument (source-reported)
Source-reported tools: argument.
Independent: unknown · difference confidence: 0
What remains uncertain
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.
VibeMath has not independently verified the mathematical claim.
AI-attempt independence and training-data exposure are unknown unless explicitly documented.
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.