Erdős problem 184 · problems.science

Any graph on $n$ vertices can be decomposed into $O(n)$ many edge-disjoint cycles and edges.

Sources

Browse retained paths and inspect the exact material available for this Problem.

6 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

184.lean

Retained formal statement5 of 6

The graph $K_{3,n-3}$ shows that at least $(1+c)n$ many cycles and edges are required, for some constant $c>0$ .

FormalConjectures/ErdosProblems/184.leanErdos184.erdos_184.variants.lower_bound5 linesExact file

1∃ c > 0,2  ∀ᶠ (n : ℕ) in Filter.atTop,3    have G := SimpleGraph.fromRel fun i j => ↑i < 3 ∧ 3 ≤ ↑j;4    ∀ (D : Finset G.Subgraph),5      (∀ H ∈ D, Erdos184.IsCycleOrEdge H.coe) → Erdos184.IsDecomposition G D → (1 + c) * ↑n ≤ ↑D.card

SolvedStatement only, no proof

Sources

Search problems.science