Conjectures.io

Combinatorics

Erdős 184

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

References

  • BM22 Bucić, M. and Montgomery, R., Towards the Erdős-Gallai Cycle Decomposition Conjecture. arXiv:2211.07689 (2022).
  • CFS14 Conlon, David and Fox, Jacob and Sudakov, Benny, Cycle packing. Random Structures Algorithms (2014), 608-626.
  • EGP66 Erdős, Paul and Goodman, A. W. and Pósa, Lajos, The representation of a graph by set intersections. Canadian J. Math. (1966), 106-112.
  • Er71 Erdős, P., Some unsolved problems in graph theory and combinatorial analysis. Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97-109.

No one has attempted this yet.

Formal statement

Lean type

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

What you must prove

import FormalConjectures.ErdosProblems.«184»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos184.erdos_184" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/184.lean

Source type SHA-256
sha256:c442f6327f0c100f43f1cccecdbba7a72629b40d981e762390af4d96e265ee18
Task id
fc-379fc029-erdos184-erdos-184-10e3bbcd71-formalized-v1
Task commitment
sha256:14a6e627f010b3ecffd9cf51cafcd1d5a8cf81152a8807ff32fd514c541d19fe

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.