Let $n\ge 3$ and $G$ be a graph with $\left(\genfrac{}{}{0ex}{}{2n+1}{2}\right)-\left(\genfrac{}{}{0ex}{}{n}{2}\right)-1$ edges. Must $G$ be the union of a bipartite graph and a graph with maximum degree less than $n$?

AMS 5 · solved (literature)

theorem erdos_613 :
    answer(False) ↔
      ∀ n ≥ 3, ∀ (V : Type*) [Fintype V] (G : SimpleGraph V), [DecidableRel G.Adj] →
        G.edgeFinset.card = Nat.choose (2 * n + 1) 2 - Nat.choose n 2 - 1 →
        ∃ (B D : SimpleGraph V), [DecidableRel B.Adj] → [DecidableRel D.Adj] →
          G = B ⊔ D ∧ B.IsBipartite ∧ ∀ v, D.degree v < n