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 statement1 of 4

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

This problem was first solved in the affirmative by Conlon, Fox, and Sudakov [CFS14b]. A simple proof is given by Hunter in the comments.

FormalConjectures/ErdosProblems/1008.leanErdos1008.erdos_10084 linesExact file

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

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science