Erdős Problem 548

Read formalization.yaml

method

autonomous — GPT-6 Astra (pre-release version, OpenAI)

review

other — mechanically verified (comparator: lean kernel replay, standard axioms only) in the benchmark harness and again in this repository's ci; preliminary informal reading of the argument by thomas f. bloom; no independent refereeing (Thomas F. Bloom)

sorry

0 unproved goals declared

sources

Proof of Erdős problem #548: Every graph on n ≥ k+1 vertices with at least (k−1)n/2 + 1 edges contains every tree on k+1 vertices. — other; Erdős problem #548 (erdosproblems.com) — background; Extremal problems in graph theory — background; FrontierMath Erdős — background

related

epoch-research/LeanOpenProblems/blob/77882c437ca1dfefab3b27fa00f1d29788100311/apn/data/erdos_autoformalized/Isolated/Erdos548.erdos_548.lean — builds-on

divergences

Relative to the cited source (the erdosproblems.com statement) there is no divergence: the compared theorem is its direct formalisation, with trees on `k+1` vertices and the hypothesis `|E| ≥ (k-1)n/2 + 1`. Relative to the classical phrasing of the Erdős–Sós conjecture ("more than `(t-2)n/2` edges, trees on `t` vertices"; here `t = k+1`) there is one marginal difference: when `(k-1)n` is odd, `|E| > (k-1)n/2` already holds with one edge fewer than `|E| ≥ (k-1)n/2 + 1` requires, so in that parity case the compared theorem assumes half an edge more and is very slightly weaker than the classical statement (the classical statement implies it, not conversely). The Lean proof's internal counting lemma derives `2|E(G)| ≤ (k-1)n` whenever the tree is absent, which is the sharp classical bound, but only the advertised statement is compared. The vertex type `Fin n` loses no generality; `G.edgeSet.ncard` is the number of edges; `T.IsTree` and `T.IsContained G` are Mathlib's notions (containment as a not necessarily induced subgraph); `k + 1 ≤ n` is `n ≥ k+1`.

checked by

nobody independent of its authors yet