Erdős problem 613

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$ ?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

613.lean

Retained formal statement1 of 1

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$ ?

FormalConjectures/ErdosProblems/613.leanErdos613.erdos_6136 linesExact file

1False ↔2  ∀ n ≥ 3,3    ∀ (V : Type u_1) [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj],4      G.edgeFinset.card = (2 * n + 1).choose 2 - n.choose 2 - 1 →5        ∃ B D,6          ∀ [DecidableRel B.Adj] [inst_3 : DecidableRel D.Adj], G = B ⊔ D ∧ B.IsBipartite ∧ ∀ (v : V), D.degree v < n

SolvedStatement only, no proof