---

Claim. In the letters of Problem 1079: if a graph on $n$ vertices has more than $\mathrm{ex}(n;K_r)$ edges, $r\ge3$, then the neighborhood of every vertex of maximum degree $m$ induces more than $\mathrm{ex}(m;K_{r-1})$ edges. This is Theorem 2 (p. 110) of J. A. Bondy, Large dense neighbourhoods and Turán's theorem, J. Combin. Theory Ser. B 34 (1983), no. 1, 109--111, with its erratum, J. Combin. Theory Ser. B 35 (1983), no. 1, 80, which corrects the note's final sentence and clarifies the definition of $S$ in the proof of Theorem 2; the note writes $t_r(n)$ for $\mathrm{ex}(n;K_{r+1})$. It answers Erdős's own formulation, graphs with $f_r(n)=\mathrm{ex}(n;K_r)+1$ edges and a star spanning at least $f_{r-1}(m)$ edges, and identifies the vertex as any vertex of maximum degree. The degree is linear in $n$, as the question asks, since the maximum degree is at least the average degree, which exceeds $2\,\mathrm{ex}(n;K_r)/n\ge(1-\frac1{r-1})n-\frac{r-1}{4n}$; that observation is the problem page's, the note stating no degree bound. The proof is twelve lines from the edge count of a complete multipartite graph. The note's examples (pp. 110--111), complete multipartite graphs with exactly $\mathrm{ex}(n;K_r)$ edges that are not Turán graphs and whose maximum-degree vertices lack the strict conclusion, show that "more than" cannot be weakened to "at least" in the hypothesis while the conclusion stays strict.

Covers. Graphs with more than $\mathrm{ex}(n;K_r)$ edges, that is, Erdős's formulation of the question, with the stronger conclusion that any vertex of maximum degree serves. Not covered by the theorem as stated: graphs with exactly $\mathrm{ex}(n;K_r)$ edges, which the site's wording includes; there the Turán graph meets the site's conclusion with equality and every other graph has a suitable vertex by the 1981 theorem on the claim page Bollobás and Thomason, which the note restates as its Theorem 1. The note's examples show only that at exactly $\mathrm{ex}(n;K_r)$ edges a maximum-degree vertex can miss the strict conclusion, Erdős's "$+1$". For the site's conclusion, at least $\mathrm{ex}(d;K_{r-1})$ edges, a vertex of maximum degree always works, by the note's argument with the inequality relaxed (an observation of this page): if a maximum-degree vertex $v$ of degree $m$ had fewer than $\mathrm{ex}(m;K_{r-1})$ edges in its neighborhood, then, every vertex outside the neighborhood having degree at most $m$, $e(G)\le(n-m)m+e(G[N(v)])<(n-m)m+\mathrm{ex}(m;K_{r-1})\le\mathrm{ex}(n;K_r)$, the middle quantity being the edge count of a complete $(r-1)$-partite graph on $n$ vertices, against the hypothesis $e(G)\ge\mathrm{ex}(n;K_r)$. The same non-strict maximum-degree form at the threshold is the theorem erdos_problem_1079 of the external Lean development described next.

Formalization. Formal-conjectures states this strengthening as erdos_1079.variants.bondy in its statement file ErdosProblems/1079.lean (proof sorry), and its formal_proof attribute names the theorem erdos_1079 of the external Lean development in Boris Alexeev's repository plby/lean-proofs, which declares itself a formalization of Bollobás and Thomason's solution and is linked from their claim page; that theorem proves, for $r\ge4$ and $n\ge2$, that more than $\mathrm{ex}(n;K_r)$ edges give a maximum-degree vertex $v$ with $n\le2\deg v$ and more than $\mathrm{ex}(\deg v;K_{r-1})$ edges in its neighborhood. The corpus has not built or audited the file, so it is no formalized evidence for this claim.

Depends on. Nothing in this wiki; the twelve-line proof is self-contained.

Acceptance. Refereed: Journal of Combinatorial Theory, Series B (the Crossref record: volume 34, issue 1, pp. 109--111, issued February 1983; the day is the issue's nominal first day, used for this page's date), with the erratum in volume 35. Reviewed: the site's curator, T. F. Bloom, labels the problem solved and credits Bondy with the strengthening in the commentary. The source card cites the publication, describes the publisher's version with its erratum and holds no file; nothing is independently reviewed. The acceptance recorded here rests on the publication and the site's acceptance, not on a local review. The site labels the problem SOLVED; since the result is a proof, the claim value here is proved, and the problem page's Status sentence keeps the site's label.