Erdős Problem 85

Reference: erdosproblems.com/85

noncomputable def Erdos85.f (n : ℕ) : ℕ

Let $f(n)$ be the smallest integer for which every graph on $n$ vertices with minimal degree $\geq f(n)$ contains a $C_4$.

Equations

• Erdos85.f n = sInf {k : ℕ | ∀ (G : SimpleGraph (Fin n)), G.minDegree ≥ k → (SimpleGraph.cycleGraph 4).IsContained G}

theorem Erdos85.erdos_85 : (∀ (n : ℕ), f (n + 1) ≥ f n) ↔ sorry

Is it true that f(n + 1) ≥ f(n)?