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 statement2 of 3

He, Ma, and Yang [HeMaYa21] proved the conjecture when $n = q^2 + q + 1$ for some even integer $q$ .

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

1∃ c > 0,2  ∀ (q : ℕ),3    Even q →4      ∀ (G : SimpleGraph (Fin (q ^ 2 + q + 1))) [inst : DecidableRel G.Adj],5        SimpleGraph.extremalNumber (q ^ 2 + q + 1) (SimpleGraph.cycleGraph 4) < G.edgeFinset.card →6          c * √(↑q ^ 2 + ↑q + 1) ≤ ↑{H' | Nonempty (H'.coe ≃g SimpleGraph.cycleGraph 4)}.ncard

SolvedStatement only, no proof