Erdős Problem 583

Conjecture 583 · Erdős

Every connected graph on $n$ vertices can be partitioned into at most $\lceil n/2\rceil$ edge-disjoint paths.

A problem of Erdős and Gallai.

Formal statement · Lean 4.lean

theorem erdos_583 {V : Type*} [Fintype V] (G : SimpleGraph V) (hG : G.Connected) :
    ∃ D : Finset G.Subgraph,
      (∀ H ∈ D, IsPathSubgraph H) ∧
      IsDecomposition G D ∧
      D.card ≤ ⌈(Fintype.card V : ℚ) / 2⌉₊ := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗