Skip to content

Erdős problem 184

Start work

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

Sources

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

184.lean

Retained formal statement5 of 6

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

FormalConjectures/ErdosProblems/184.leanErdos184.erdos_184.variants.lower_bound5 linesExact file
∃ c > 0,  ∀ᶠ (n : ℕ) in Filter.atTop,    have G := SimpleGraph.fromRel fun i j => ↑i < 3 ∧ 3 ≤ ↑j;    ∀ (D : Finset G.Subgraph),      (∀ H ∈ D, Erdos184.IsCycleOrEdge H.coe) → Erdos184.IsDecomposition G D → (1 + c) * ↑n ≤ ↑D.card
SolvedStatement only, no proof