Erdős Problem 572

Conjecture 572 · Erdős

Show that for $k\geq 3$ $\mathrm{ex}(n;C_{2k})\gg n^{1+\frac{1}{k}}.$

This problem is #46 in Extremal Graph Theory in the graphs problem collection.

Formal statement · Lean 4.lean

theorem erdos_572 (k : ℕ) (hk : 3 ≤ k) :
    ∃ c > (0 : ℝ), ∀ᶠ (n : ℕ) in atTop,
      c * (n : ℝ) ^ (1 + 1 / (k : ℝ)) ≤
        (SimpleGraph.extremalNumber n (SimpleGraph.cycleGraph (2 * k)) : ℝ) := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗