Skip to content

Erdős problem 1008

Start work

Does every graph with mm edges contain a subgraph with ≫m2/3\gg m^{2/3} edges which contains no C4C_4?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1008.lean

Retained formal statement1 of 4

Does every graph with mm edges contain a subgraph with ≫m2/3\gg m^{2/3} edges which contains no C4C_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
True ↔  ∃ c > 0,    ∀ (V : Type) [Fintype V] (G : SimpleGraph V),      ∃ 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.