Erdős Problem 613 #
Reference: erdosproblems.com/613
theorem
Erdos613.erdos_613 :
False ↔ ∀ n ≥ 3,
∀ (V : Type u_1) [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj],
G.edgeFinset.card = (2 * n + 1).choose 2 - n.choose 2 - 1 →
∃ (B : SimpleGraph V) (D : SimpleGraph V),
∀ [DecidableRel B.Adj] [inst_3 : DecidableRel D.Adj], G = B ⊔ D ∧ B.IsBipartite ∧ ∀ (v : V), D.degree v < n
Erdős Problem 613: Let $n \geq 3$ and $G$ be a graph with $\binom{2n+1}{2} - \binom{n}{2} - 1$ edges. Must $G$ be the union of a bipartite graph and a graph with maximum degree less than $n$?