Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 1079
claims/: The 2 claim pages of Problem 1079, one per claimant's result; the problem's standing derives from them.
Statement. Let . If is a graph on vertices with at least edges then must contain a vertex with degree whose neighbourhood contains at least edges?
Formulation. The site's wording as of 2026-09-18 (page last edited 14 October 2025). is the Turán number, the largest number of edges of a -free graph on vertices, attained by the Turán graph ; "degree " asks for with a constant depending on alone; "neighborhood" is the set of vertices joined to the vertex, and the edges counted are those of the subgraph it induces. Erdős's 1975 wording differs in two places (Er75, p. 14): he asks it for graphs , where is the least number of edges forcing a , that is edges, and asks the star to span at least edges, so that the neighborhood contains a and the graph a , which is the sense of his "If true this would be a nice generalization of Turán's theorem"; the site's version drops both ""s. Two observations, this page's own, about the site's version. First, its conclusion is satisfied by the Turán graph itself: the neighborhood of any vertex is the union of the other classes, whose sizes differ by at most one, so it induces the Turán graph with exactly edges and ; the exception the site makes for the Turán graph itself therefore belongs to a statement with a strict inequality somewhere, and [BoTh81] supplies it: its theorem (BoTh81, Theorem, p. 111) takes a graph with at least edges and concludes that either is the Turán graph or some vertex has at least edges in its neighborhood, Erdős's "", with (the paper writes for the number of parts of the Turán graph, one less than the here). [Bo83b] restates that theorem, in the same indexing, as its Theorem 1 (p. 109), with the hypothesis "at least edges" and the conclusion "either or there is a vertex " whose neighborhood induces "more than edges", which is the 1981 paper's "" in other words; Bondy's own Theorem 2 has "more than" in both places (the Status). Second, the site's label SOLVED, which the site glosses as a resolution by neither a proof nor a disproof, attaches to a yes-or-no question that the commentary answers affirmatively; the claim pages record the result as proved, and the frontmatter standing derives from them. The thread's first comment (7 October 2025) reads the intended statement as asking for a set of vertices inside some neighborhood with edges, and the site's curator agreed that this was presumably Erdős's intent; the statement itself was not changed. Under that reading the answer is also yes: take for the vertex of the Bollobás--Thomason theorem, with and at least edges; for the Turán graph any neighborhood has exactly edges.
Status. Solved, the site's label; the answer is yes, and the standing here is solved and proved, derived from the claim pages below. The site credits the affirmative answer, with the Turán graph as the one exception, to Bollobás and Thomason [BoTh81], credits Bondy [Bo83b] with the strengthening that for more than edges the vertex can be taken of maximum degree, and the community database records the problem as solved. The two status-defining sources are B. Bollobás and A. Thomason, "Dense neighbourhoods and Turán's theorem", J. Combin. Theory Ser. B 31 (1981), no. 1, 111--114, and J. A. Bondy, "Large dense neighbourhoods and Turán's theorem", J. Combin. Theory Ser. B 34 (1983), no. 1, 109--111 (both refereed, per their Crossref records). Neither source card holds a file. [BoTh81] (library home bollobas_thomason_1981_dense_neighbourhoods_turan_s_theorem, the publisher's open-archive version) carries the affirmative answer in its theorem (printed p. 111), paged at theorem_p111, in the paper's indexing with the -partite Turán graph and its number of edges: "Let be a graph of order with edges. Then either or else there is a vertex such that , the subgraph spanned by the neighbours of , contains at least edges, where . Furthermore ." With this is the site's statement in the paper's letters, with the "" of Erdős's question in the conclusion, the Turán graph the only exception, and an explicit constant, in the site's indexing (). The paper attributes the conjecture to [Er75], its [2], in the form "if " (p. 111). Its proof (pp. 112--114) is followed on the card, which records four observations (three misprints and a final inequality that needs in the paper's ). [Bo83b] (library home bondy_1983_large_dense_neighbourhoods_turan_s_theorem, the publisher's version with its erratum) carries Bondy's own strengthening as its Theorem 2 (p. 110), paged at theorem_2, in the same indexing: "Let be a simple graph on vertices and more than edges, where , and let be a vertex in of degree . Then the subgraph induced by the neighbours of has more than edges"; its proof is twelve lines. In the problem's letters: more than edges, Erdős's , force every vertex of maximum degree to have a neighborhood with more than edges, Erdős's "at least "; the maximum degree is at least the average degree, which is more than , so the degree is linear (this page's own observation; the note states no degree bound for its own theorem). The note also states the theorem of [BoTh81] as its Theorem 1 (p. 109), paged at theorem_1, with the attribution "proved independently by Bollobás and Thomason [1] and Erdős and Sós [4]" and the degree bound as its (1); the restatement agrees with the 1981 theorem, its "more than edges" being that paper's "at least edges", and it names a second proof, an Erdős--Sós preprint, which is not among this page's sources. Bondy's examples (p. 111), graphs with exactly edges that are not Turán graphs and whose maximum-degree vertices do not have the strict conclusion, show that the "" of the site's account of [Bo83b] cannot be weakened for that conclusion; for the site's non-strict conclusion a maximum-degree vertex always works, as the Bondy claim page records. Nothing here is independently reviewed. The site's label SOLVED attaches to an affirmative answer proved in two refereed notes; the claim pages (Bollobás and Thomason, full, and Bondy, partial, for graphs with more than edges) record the result as proved.
Source. erdosproblems.com/1079, accessed 2026-09-18: the problem page (SOLVED, glossed by the site as a resolution by neither a proof nor a disproof; last edited 14 October 2025; source keys [Bo83b], [BoTh81], [Er75]; commentary quoting [Er75] and citing [BoTh81] and [Bo83b]), its three-comment discussion thread (7 and 13 October 2025) and its empty proof-claim tab. Cite as: T. F. Bloom, Erdős Problem #1079, https://www.erdosproblems.com/1079, accessed 2026-09-18.
References.
- [BoTh81] Bollobás, Béla and Thomason, Andrew, Dense neighbourhoods and Turán's theorem. J. Combin. Theory Ser. B 31 (1981), no. 1, 111--114, doi:10.1016/S0095-8956(81)80016-0 (issued August 1981; the Crossref record carries the publisher's open-archive license and no abstract); the Theorem and the introduction, printed p. 111; the proof, printed pp. 112--114. Library home: bollobas_thomason_1981_dense_neighbourhoods_turan_s_theorem (the publisher's open-archive version; no file is held); the theorem is paged at theorem_p111.
- [Bo83b] Bondy, J. A., Large dense neighbourhoods and Turán's theorem. J. Combin. Theory Ser. B 34 (1983), no. 1, 109--111, doi:10.1016/0095-8956(83)90012-6 (received February 21, 1981, per p. 109; issued February 1983), with its erratum, J. Combin. Theory Ser. B 35 (1983), no. 1, 80, doi:10.1016/0095-8956(83)90082-5, which corrects the note's final sentence and clarifies the definition of in the proof of Theorem 2. Theorem 1 and the degree bound (1), p. 109; Theorem 2 with its proof, p. 110; the examples and the final sentence, pp. 110--111; the publisher's version with its erratum, of which no file is held. Library home: bondy_1983_large_dense_neighbourhoods_turan_s_theorem; the results are paged at theorem_1 (the Bollobás--Thomason theorem as restated) and theorem_2.
- [Er75] Erdős, P., Some recent progress on extremal problems in graph theory. Congr. Numer. XIV (1975), 3--14; Chapter 4, printed p. 14. Library home: erdos_1975_recent_progress_extremal_problems_graph_theory; the passage is paged at problem_p14.
- [BoNi05] Bollobás, B. and Nikiforov, V., The sum of degrees in cliques. Electron. J. Combin. 12 (2005), N21. Not a site key for this problem; its introduction carries no attestation of [BoTh81] or [Bo83b]. Library home: bollobas_2005_sum_degrees_cliques.
Formalization. A statement file and an external proof, neither built by the
corpus. Formal-conjectures added
ErdosProblems/1079.lean
on 2026-09-19 (no such file existed at main on 2026-09-18); the link pins the
commit that added it, which is the one described. It declares
erdos_1079 : answer(True) ↔ ... under category research solved, with proof
sorry: for every there is such that every graph on
vertices with at least edges has a vertex with
and at least edges of with
both ends adjacent to . Beside it, erdos_1079.variants.bondy states Bondy's
strengthening, that more than edges give a vertex of
maximum degree with and more than
edges in its neighborhood, also with proof sorry, and its formal_proof
attribute names line 424 of the file src/latest/ErdosProblems/Erdos1079.lean
in Boris Alexeev's repository plby/lean-proofs at a commit of 15 September 2026.
That external file (441 lines, toolchain Lean v4.33.0, first added on
2026-08-17) declares itself a Lean formalization of a solution to Problem 1079,
names Béla Bollobás and Andrew Thomason as its informal authors and Codex and
GPT-5.6 Sol as its formal authors, and proves two theorems:
erdos_problem_1079, that for , and at least
edges some vertex of maximum degree has and at
least edges in its neighborhood, and erdos_1079, the
strict form for more than edges, the target of the
formal_proof attribute; the file carries no sorry and ends by printing the
axioms of both theorems. Since it names those authors, it is a formalization
link on
Bollobás and Thomason's claim page
and not a claim of its own; the corpus has not built or audited it, so no
formalized evidence is recorded. The site showed no formalized statement on
2026-09-18 and shows one since; the community database (teorth/erdosproblems,
data/problems.yaml,) records the problem solved (last update
14 October 2025) and its statement formalized since 19 September 2026, with
formal_status unformalized.
Current assessment
The question (site formulation of 2026-09-18). The statement above; SOLVED; last edited 14 October 2025. The commentary, in the corpus's words: it repeats Erdős's remark that a positive answer would generalize Turán's theorem, states that the answer is yes unless is the Turán graph itself, proved by Bollobás and Thomason [BoTh81], and that Bondy [Bo83b] showed the vertex can be taken of maximum degree when has more than edges. The thread: a comment of 7 October 2025 (the account zach hunter) on the intended reading (a neighborhood set of size with edges) and the site author's agreement the same day; a comment of 13 October 2025 (the account msawhney) giving the two publishers' article pages with their journal issues (JCTB August 1981, vol. 31, issue 1; JCTB February 1983, vol. 34, issue 1), restating Bondy's strengthening for graphs with edges, and saying the reference was located by GPT-5 Pro. The proof-claim tab is empty. The community database record says solved (14 October 2025).
Status support. The support for the site's label is of two kinds, and the first is the mathematics itself. The theorem of [BoTh81] (p. 111, the statement; pp. 112--114, the proof) answers the site's question affirmatively for every , with the "" in the conclusion, the Turán graph as the only exception and an explicit constant; Theorem 2 of [Bo83b] (p. 110), with its twelve-line proof, answers Erdős's own formulation ( edges, a star with at least edges) for any vertex of maximum degree, and Theorem 1 of the same note (p. 109) restates the 1981 theorem with the degree bound (1), a second printed statement of the same theorem. Both notes are short refereed papers in the Journal of Combinatorial Theory, Series B, confirmed by Crossref (four and three pages). The catalog's acceptance: the label with its gloss, the attribution to Bollobás--Thomason with Bondy's strengthening, and the community database's record of the problem as solved. Two citing papers in the citation lists, "Turán's theorem and maximal degrees" (J. Combin. Theory Ser. B, 1999, doi:10.1006/jctb.1998.1873) and Faudree's Complete subgraphs with large degree sums (J. Graph Theory 16 (1992)), each cite both notes; neither is a source of this page, and with the theorems stated in the notes themselves neither is needed as a second-hand attestation. The same lists carry a run of 2022--2026 spectral Turán papers citing the two notes for context. The one further proof of the theorem named in the notes is the Erdős--Sós preprint that Bondy credits alongside [BoTh81] for his Theorem 1; the note gives it no title. The site's label SOLVED, glossed as a resolution by neither a proof nor a disproof, sits on a yes-or-no question answered affirmatively by two refereed theorems; the claim pages therefore carry the value proved, and the Status sentence keeps the site's label.
The theorem. The Theorem of [BoTh81] (printed p. 111), quoted in the Status above, counts triangles against the degree sequence: with triangles and degrees , the paper derives with equality exactly for complete multipartite graphs (p. 112), defines a function that equals for and is quadratic below, and shows that if no vertex of degree lies in more than triangles then the resulting inequality forces the degree sequence of and equality above, that is, (p. 113). Otherwise some vertex of degree lies in at least triangles, which are the edges of its neighborhood, and the quadratic form of below gives the degree bound (pp. 113--114). The card records four observations on the printed proof (a "" printed for "" on p. 112, an "" printed for "" on p. 114, a last inequality on p. 114 that holds exactly when in the paper's , with equality at that value, so that the bound is proved for , which does not affect the existence of and leaves a positive constant for every since lies in a triangle, and a "" printed for "" in the definition of on p. 112). Bondy's own Theorem 2 is proved in twelve lines from the edge count of a complete multipartite graph, with no degree bound; its proof pointer is on theorem_2. Nothing here is independently reviewed.
The origin in Erdős's words. [Er75], printed p. 14 (problem_p14): with the least number of edges forcing a in a graph on vertices and the star of a vertex its set of neighbors: "Is there a constant so that every has a vertex of valency so that the graph spanned by its star has at least edges?", adding that a positive answer "would be a nice generalization of Turán's theorem" and that he could not settle the first interesting case, . The question is asked for edges and for a star with edges; the site's statement has "at least " and "at least " (the Formulation note). The survey gives no partial result. [BoTh81] cites it as its [2] and restates the conjecture with the strict inequality, "if then there is a vertex in with such that ... contains at least edges" (p. 111), which is Erdős's edges in the paper's indexing; its theorem weakens the hypothesis to and excepts the Turán graph. Bondy's Theorem 2 answers Erdős's question as he asked it, for graphs with edges, and identifies the vertex as any of maximum degree.
Search scope. None of the routes below found a dispute of either theorem or a later paper on the question itself. The versions consulted are the publisher's open-archive version of [BoTh81] and the publisher's version of [Bo83b] with its erratum.
- The site: problem page, discussion thread and proof-claim tab; formal-conjectures at main, which had no file for the problem on 2026-09-18 (the statement file of 2026-09-19 is described under Formalization); the community database entry as of 2026-09-18.
- Crossref: the records of doi:10.1016/S0095-8956(81)80016-0 and doi:10.1016/0095-8956(83)90012-6 (volumes, issues, pages and dates; no abstracts).
- Semantic Scholar: the citing papers of [BoTh81] (fifteen records) and [Bo83b] (thirteen records), titles and venues; the 1999 JCTB paper and Faudree 1992 are the candidates named above; the rest are spectral Turán papers of 2022--2026 and two 2013 survey chapters.
- arXiv API: the search
all:Turan AND all:"neighbourhood" AND all:"maximum degree"(no records; a weak zero, the API searching titles and abstracts with uncertain handling of diacritics). - The primary sources: [Er75] p. 14; the introduction of [BoNi05] (pp. 1--2), which carries no attestation of the two notes; [BoTh81] pp. 111--114 and [Bo83b] pp. 109--111 with its erratum.
Not searched: MathSciNet, zbMATH, Google Scholar, X.
Remaining gaps. (1) Both status-defining notes are paged: the
Bollobás--Thomason theorem with its proof and the card's four observations
on it, and Bondy's Theorem 2 with its twelve-line proof, so the Formulation
questions (the "", the Turán-graph exception, the constant ) are
settled from the texts. Nothing is independently reviewed. Not needed for
the status: the Erdős--Sós preprint that Bondy credits alongside [BoTh81] for his
Theorem 1, the 1999 JCTB paper and Faudree 1992. (2) The site's statement
differs from Erdős's in both edge counts and, as it stands, is satisfied by
the Turán graph; the 1981 theorem carries the "" that makes the site's
exception meaningful, Bondy's Theorem 1 pairs the exception with the "more
than" conclusion, and the intended reading is recorded from the thread.
(3) The site's label SOLVED attaches to an affirmative answer; the claim
pages record the result as proved. (4) The Lean material is a
formal-conjectures statement with proof sorry and an external development
that proves both the non-strict maximum-degree form at the threshold and
Bondy's strict form, linked from the Bollobás--Thomason claim page; the
corpus has not built or audited it, so no formalized evidence is
recorded.
Known results
- Erdős 1975, p. 14: the question as posed, with edges and a star spanning edges.
- BoTh81, Theorem, p. 111 (1981, refereed): for a graph of order with at least edges, either or some vertex has at least edges among its neighbors, with ; the site's statement with Erdős's "" and the Turán graph as the only exception. Restated, with the degree bound as its (1), in Bondy 1983, Theorem 1 (p. 109): at least edges give the Turán graph or a vertex whose neighborhood induces more than edges, with degree .
- Bondy 1983, Theorem 2 (1983, refereed; p. 110): for more than edges every vertex of maximum degree has a neighborhood inducing more than edges; the examples of p. 111 show that at exactly edges a vertex of maximum degree can miss this strict conclusion, while for the site's non-strict conclusion a maximum-degree vertex always works (the Bondy claim page).
- The external Lean development of 2026 (a
formalizationlink on Bollobás and Thomason's claim page; not built by the corpus): for , and at least edges, a vertex of maximum degree with and at least edges in its neighborhood, and the strict form above the threshold.
Linked library material
These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.
- bollobas_thomason_1981_dense_neighbourhoods_turan_s_theorem
- bollobas_thomason_1981_dense_neighbourhoods_turan_s_theorem / theorem_p111
- bondy_1983_large_dense_neighbourhoods_turan_s_theorem
- bondy_1983_large_dense_neighbourhoods_turan_s_theorem / theorem_1
- bondy_1983_large_dense_neighbourhoods_turan_s_theorem / theorem_2
- erdos_1975_recent_progress_extremal_problems_graph_theory
- erdos_1975_recent_progress_extremal_problems_graph_theory / problem_p14