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 : True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, f n ≤ f (n + 1)

Is it true that, for all large $n$, $f(n + 1) \ge f(n)$?