Erdős problem 128

Let G be a graph with n vertices such that every induced subgraph on ≥ $n/2$ vertices has more than $n^2/50$ edges. Must G contain a triangle?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

128.lean

Retained formal statement1 of 1

Let G be a graph with n vertices such that every induced subgraph on ≥ $n/2$ vertices has more than $n^2/50$ edges. Must G contain a triangle?

FormalConjectures/ErdosProblems/128.leanErdos128.erdos_1285 linesExact file

1True ↔2  ∀ (V : Type) [inst : Fintype V] (G : SimpleGraph V),3    (∀ (V' : Set V),4        2 * V'.ncard + 1 ≥ Fintype.card V → 50 * (SimpleGraph.induce V' G).edgeSet.ncard > Fintype.card V ^ 2) →5      ¬G.CliqueFree 3

OpenStatement only, no proof