Erdős Problem 128

Reference: erdosproblems.com/128

theorem Erdos128.erdos_128 : sorry ↔ ∀ (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 3

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?