Problem

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 D, ∀ [DecidableRel B.Adj] [inst_3 : DecidableRel D.Adj], G = B ⊔ D ∧ B.IsBipartite ∧ ∀ (v : V), D.degree v < n

Open Current State

Declared status: disproved (Lean)
Formalization: formalized
Subjects: graph theory
OEIS: N/A
Sources: source:erdos-ai-contributions-wikisource:erdos-problemssource:formal-conjecturessource:jayyhk-erdos-leansource:plby-lean-proofs
Statement: www.erdosproblems.com

Matching claims

0

No direct claims

This problem has no directly related claim record.

Browse this Repository’s Claims