Skip to content

Erdős problem 1034

Let GG be a graph on nn vertices with >n2/4>n^2/4 many edges. Must there be a triangle TT in GG and vertices y1,…,yty_1,\ldots,y_t, where t>(12−o(1))nt>(\frac{1}{2}-o(1))n, such that every yiy_i is joined to at least two vertices of TT?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1034.lean

Retained formal statement3 of 4

Erdős and Faudree asked about the threshold h(n)h(n) such that every graph with nn vertices and >n2/4>n^2/4 edges contained a triangle and h(n)h(n) other vertices which are connected to at least two vertices of the triangle. The fact that every graph with >n2/4>n^2/4 edges contains a book of size n/6n/6 shows that (1/6−o(1))n≤h(n).(1/6-o(1))n \leq h(n).

FormalConjectures/ErdosProblems/1034.leanErdos1034.erdos_1034.variants.lower_bound6 linesExact file
∀ (ε : ℝ),  0 < ε →    ∀ᶠ (n : ℕ) in Filter.atTop,      ∀ (G : SimpleGraph (Fin n)),        ↑n ^ 2 / 4 < ↑G.edgeSet.ncard →          ∃ T, G.IsNClique 3 T ∧ ∃ Y, Erdos1034.JoinedToTwo G T Y ∧ (1 / 6 - ε) * ↑n ≤ ↑Y.card
SolvedStatement only, no proof