Erdős problem 128
Let G be a graph with n vertices such that every induced subgraph on ≥ vertices has more than edges. Must G contain a triangle?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/128.leanTrue ↔ ∀ (V : Type) [inst : Fintype V] (G : SimpleGraph V), (∀ (V' : Set V), 2 * V'.ncard + 1 ≥ Fintype.card V → 50 * (SimpleGraph.induce V' G).edgeSet.ncard > Fintype.card V ^ 2) → ¬G.CliqueFree 3OpenStatement only, no proof