Erdős problem 613 · problems.science

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

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/613.lean

Formal Conjectures

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

Proof manifests naming this Problem

Jayyhk Erdős Leanjayyhk:erdos:613
PLBY Lean proofsErdosProblems.Erdos613

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Formalization
Erdős AI contributions wiki · 4 Nov, 2025
Machine
GPT Pro
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science