Formal target: Corpus.Erdos60.erdos_60
Does every graph on $n$ vertices with $>\mathrm{ex}(n;C_4)$ edges contain $\gg n^{1/2}$ many copies of $C_4$?
Exact formal statement
Exists.{1} fun c =>
And (GT.gt.{0} c 0)
(Filter.Eventually.{0}
(fun n =>
∀ (G : SimpleGraph.{0} (Fin n)) [inst : DecidableRel.{1, 1} (SimpleGraph.Adj.{0} G)],
LT.lt.{0} (SimpleGraph.extremalNumber.{0} n (SimpleGraph.cycleGraph 4))
(Finset.card.{0} (SimpleGraph.edgeFinset.{0} G)) →
LE.le.{0} (HMul.hMul.{0, 0, 0} c (Nat.cast.{0} n).sqrt)
(Nat.cast.{0}
(Set.ncard.{0}
(Set.ofPred.{0} fun H' =>
Nonempty.{1}
(SimpleGraph.Iso.{0, 0} (SimpleGraph.Subgraph.coe.{0} H') (SimpleGraph.cycleGraph 4))))))
Filter.atTop.{0})This target is a formal statement, not a proof of the problem.
Environment availability: available.