Erdős problem 1008 · problems.science

Does every graph with $m$ edges contain a subgraph with $\gg m^{2/3}$ edges which contains no $C_4$ ?

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1008.lean

Retained formal statement3 of 4

In [Er71] Erdős revises the conjecture to $m^{2/3}$ , and notes $\gg m^{1/2}$ is trivial.

FormalConjectures/ErdosProblems/1008.leanErdos1008.erdos_1008.variants.lower_bound3 linesExact file

1∃ c > 0,2  ∀ (V : Type) [Fintype V] (G : SimpleGraph V),3    ∃ H ≤ G, (SimpleGraph.cycleGraph 4).Free H ∧ c * ↑G.edgeSet.ncard ^ (1 / 2) ≤ ↑H.edgeSet.ncard

SolvedStatement only, no proof

Sources

Search problems.science