Erdős–Faudree triangle conjecture

DefinitionVertices joined to two vertices of a set#✓fully proved

Let \(G\) be a simple graph on a vertex type \(V\) and let \(T\) and \(Y\) be finite sets of vertices. The set \(Y\) is joined to two vertices of \(T\) in \(G\) if every vertex \(y \in Y\) is adjacent in \(G\) to two distinct vertices \(u, v \in T\).

def JoinedToTwo {V : Type*} (G : SimpleGraph V) (T Y : Finset V) : Prop :=
  ∀ y ∈ Y, ∃ u ∈ T, ∃ v ∈ T, u ≠ v ∧ G.Adj y u ∧ G.Adj y v

Used by 4

Used byBook lower bound for Erdős Problem 1034 · Erdős–Faudree triangle conjecture · \(K_4\)-free upper bound for Erdős Problem 1034 · Ma–Tang upper bound for Erdős Problem 1034

DefinitionErdős–Faudree triangle conjecture#✓fully proved

For every real \(\varepsilon > 0\) the following holds for all sufficiently large \(n\): every simple graph \(G\) on the vertex set \(\{0, \dots, n-1\}\) with more than \(n^2/4\) edges contains a triangle \(T\) and a set \(Y\) of vertices, each adjacent in \(G\) to two distinct vertices of \(T\), with \(|Y| > (1/2 - \varepsilon)n\).

This claim (Erdős Problem 1034) was disproved by Ma and Tang.

def conjecture : Prop :=
  ∀ ε : ℝ, 0 < ε → ∀ᶠ (n : ℕ) in atTop, ∀ G : SimpleGraph (Fin n),
    (n : ℝ) ^ 2 / 4 < (G.edgeSet.ncard : ℝ) →
      ∃ T : Finset (Fin n), G.IsNClique 3 T ∧ ∃ Y : Finset (Fin n),
        JoinedToTwo G T Y ∧ (1 / 2 - ε) * (n : ℝ) < (Y.card : ℝ)

Uses 1 · Used by 2

Statement usesVertices joined to two vertices of a set

Used byThe Erdős–Faudree triangle conjecture is false · Negation of the Erdős–Faudree triangle conjecture

DefinitionNegation of the Erdős–Faudree triangle conjecture#✓fully proved

The proposition that the Erdős–Faudree triangle conjecture fails, that is, that it is not the case that for every real \(\varepsilon > 0\) and all sufficiently large \(n\), every simple graph \(G\) on the vertex set \(\{0, \dots, n-1\}\) with more than \(n^2/4\) edges contains a triangle \(T\) and a set \(Y\) of vertices, each adjacent in \(G\) to two distinct vertices of \(T\), with \(|Y| > (1/2 - \varepsilon)n\).

def disprovedForm : Prop := ¬ conjecture

Uses 1

Statement usesErdős–Faudree triangle conjecture

DefinitionBook lower bound for Erdős Problem 1034#✓fully proved

For every real \(\varepsilon > 0\) the following holds for all sufficiently large \(n\): every simple graph \(G\) on the vertex set \(\{0, \dots, n-1\}\) with more than \(n^2/4\) edges contains a triangle \(T\) and a set \(Y\) of vertices, each adjacent in \(G\) to two distinct vertices of \(T\), with \(|Y| \ge (1/6 - \varepsilon)n\).

def bookLowerBound : Prop :=
  ∀ (ε : ℝ), 0 < ε →
    ∀ᶠ (n : ℕ) in atTop, ∀ G : SimpleGraph (Fin n),
      (n : ℝ) ^ 2 / 4 < (G.edgeSet.ncard : ℝ) →
        ∃ T : Finset (Fin n), G.IsNClique 3 T ∧ ∃ Y : Finset (Fin n),
          JoinedToTwo G T Y ∧ (1 / 6 - ε) * (n : ℝ) ≤ (Y.card : ℝ)

Uses 1

Statement usesVertices joined to two vertices of a set

DefinitionMa–Tang upper bound for Erdős Problem 1034#✓fully proved

For every real \(\varepsilon > 0\) the following holds for all sufficiently large \(n\): there is a simple graph \(G\) on the vertex set \(\{0, \dots, n-1\}\) with more than \(n^2/4\) edges such that for every triangle \(T\) of \(G\), every set \(Y\) of vertices each adjacent in \(G\) to two distinct vertices of \(T\) satisfies \(|Y| \le (2 - \sqrt{5/2} + \varepsilon)n\).

def maTangUpperBound : Prop :=
  ∀ (ε : ℝ), 0 < ε →
    ∀ᶠ (n : ℕ) in atTop, ∃ G : SimpleGraph (Fin n),
      (n : ℝ) ^ 2 / 4 < (G.edgeSet.ncard : ℝ) ∧
        ∀ T : Finset (Fin n), G.IsNClique 3 T → ∀ Y : Finset (Fin n),
          JoinedToTwo G T Y →
          (Y.card : ℝ) ≤ (2 - Real.sqrt (5 / 2) + ε) * (n : ℝ)

Uses 1

Statement usesVertices joined to two vertices of a set

Definition\(K_4\)-free upper bound for Erdős Problem 1034#✓fully proved

For every real \(\varepsilon > 0\) the following holds for all sufficiently large \(n\): there is a simple graph \(G\) on the vertex set \(\{0, \dots, n-1\}\) that contains no \(K_4\) and has more than \(n^2/4\) edges, such that for every triangle \(T\) of \(G\), every set \(Y\) of vertices each adjacent in \(G\) to two distinct vertices of \(T\) satisfies \(|Y| \le (2\sqrt{3} - 3 + \varepsilon)n\).

def k4FreeUpperBound : Prop :=
  ∀ (ε : ℝ), 0 < ε →
    ∀ᶠ (n : ℕ) in atTop, ∃ G : SimpleGraph (Fin n), G.CliqueFree 4 ∧
      (n : ℝ) ^ 2 / 4 < (G.edgeSet.ncard : ℝ) ∧
        ∀ T : Finset (Fin n), G.IsNClique 3 T → ∀ Y : Finset (Fin n),
          JoinedToTwo G T Y →
          (Y.card : ℝ) ≤ (2 * Real.sqrt 3 - 3 + ε) * (n : ℝ)

Uses 1

Statement usesVertices joined to two vertices of a set

TheoremThe Erdős–Faudree triangle conjecture is false#●ready to prove

It is not true that for every real \(\varepsilon > 0\) and all sufficiently large \(n\), every simple graph on the vertex set \(\{0, \dots, n-1\}\) with more than \(n^2/4\) edges contains a triangle \(T\) and a set of more than \((1/2 - \varepsilon)n\) vertices, each adjacent to two distinct vertices of \(T\).

public theorem_wanted conjecture_refuted : ¬ conjecture

Sources

• Ma and Tang (disproof with upper bound (2-√(5/2)+o(1))n; K₄-free sketch with (2√3-3+o(1))n), per erdosproblems.com/1034, https://www.erdosproblems.com/1034.

Uses 1

Statement usesErdős–Faudree triangle conjecture

6 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.