Erdős Problem 128

Reference: erdosproblems.com/128

theorem Erdos128.erdos_128 {V : Type u_1} {G : SimpleGraph V} [Fintype V] : (∀ (G' : G.Subgraph) [inst : Fintype ↑G'.verts] [inst_1 : Fintype ↑G'.edgeSet], 2 * G'.verts.toFinset.card ≥ Fintype.card V → 50 * G'.edgeSet.toFinset.card > 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?