Erdős problem 60

Does every graph on $n$ vertices with $>\mathrm{ex}(n;C_4)$ edges contain $\gg n^{1/2}$ many copies of $C_4$ ?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

60.lean

Retained formal statement3 of 3

Erdős and Simonovits conjectured that at least 2 copies of $C_4$ are guaranteed.

FormalConjectures/ErdosProblems/60.leanErdos60.erdos_60.variants.two_copies4 linesExact file

1∀ᶠ (n : ℕ) in Filter.atTop,2  ∀ (G : SimpleGraph (Fin n)) [inst : DecidableRel G.Adj],3    SimpleGraph.extremalNumber n (SimpleGraph.cycleGraph 4) < G.edgeFinset.card →4      2 ≤ {H' | Nonempty (H'.coe ≃g SimpleGraph.cycleGraph 4)}.ncard

SolvedStatement only, no proof