Erdős Problem 128

Reference: erdosproblems.com/128

theorem Erdos128.erdos_128 {V : Type u_1} {G : SimpleGraph V} [Fintype V] : (∀ (V' : Set V), 2 * V'.ncard ≥ Fintype.card V → 50 * (SimpleGraph.induce V' G).edgeSet.ncard > Fintype.card V ^ 2) → ¬G.CliqueFree 3 ↔ sorry

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