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

FormalConjectures/ErdosProblems/

184.lean

Retained formal statement2 of 6

The best bound available is due to Bucić and Montgomery [BM22], who prove that $O(n\log^* n)$ many cycles and edges suffice, where $\log^*$ is the iterated logarithm function.

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

1∃ f,2  (f =O[Filter.atTop] fun n => ↑n * ↑(↑n).iteratedLog) ∧3    ∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V),4      ∃ D, (∀ H ∈ D, Erdos184.IsCycleOrEdge H.coe) ∧ Erdos184.IsDecomposition G D ∧ ↑D.card ≤ f (Fintype.card V)

SolvedStatement only, no proof

Sources

Search problems.science