Erdős–Gallai conjecture: decompose any n-vertex graph into O(n) edge-disjoint cycles and edges (Erdős #184)
Statement
Prove or disprove: there is an absolute constant $C>0$ such that the edge set of every graph $G$ on $n$ vertices can be partitioned into at most $Cn$ parts, each of which is either a cycle of $G$ or a single edge. (Equivalently: any graph on $n$ vertices can be decomposed into $O(n)$ many edge-disjoint cycles and edges.)
Acceptance. FULLY RESOLVES: a complete proof that some absolute constant $C$ works for all $n$-vertex graphs — machine-checkable (Lean/Coq) preferred, otherwise a full written proof with all steps and explicit or effective constants; OR a disproof: an explicit infinite family of graphs together with a proof that any decomposition into edge-disjoint cycles and single edges requires $\omega(n)$ parts. A computation alone cannot close this asymptotic statement. ADVANCES: (a) a proof improving the best upper bound stated in the background (currently $O(n\log^* n)$ parts) to a strictly smaller growth rate, with complete proof; (b) extending the linear bound from minimum degree $\epsilon n$ to a strictly wider class of graphs (e.g. polynomial degeneracy or sublinear minimum-degree regimes), with proof; (c) improving the lower-bound constant $c$ in the $(1+c)n$ bound with an explicit certified construction family; (d) a machine-verified (Lean) formalization of one of the frontier results ([EGP66] $O(n\log n)$ or the dense case). Deliver the proof file (or Lean sources that compile), and for constructions the family definition plus the counting proof.
Background
Conjectured by Erdős and Gallai; Erdős returned to it repeatedly [EGP66, Er71, Er76, Er81, Er83b], and it is listed as open on erdosproblems.com/184 (fetched 2026-07-13, status 'open', tagged 'graph theory | cycles'). Erdős, Gallai and Pósa proved that $O(n\log n)$ cycles and edges always suffice (Section 5 of [EGP66]). The current record is due to Bucić and Montgomery [BM22], who proved that $O(n\log^* n)$ cycles and edges suffice, where $\log^*$ is the iterated logarithm — tantalizingly close to linear but not yet there. Conlon, Fox, and Sudakov [CFS14] proved the conjecture for dense graphs: $O_\epsilon(n)$ parts suffice whenever $G$ has minimum degree at least $\epsilon n$. In the other direction, the complete bipartite graph $K_{3,n-3}$ shows that $(1+c)n$ parts are needed for some constant $c>0$, so the conjectured bound cannot be improved below a nontrivial multiple of $n$. Erdős [Er71] also suggested that $n-1$ cycles and edges suffice if the edge-disjointness requirement is dropped (a covering variant). The path analogue is Erdős #583 (erdosproblems.com/583), and the venue hosts the closely related Gallai path decomposition conjecture (every connected $n$-vertex graph splits into $\lceil n/2\rceil$ paths) as a separate problem; #184 is the cycles-and-edges decomposition question and is not settled by either. The attacker's tool here is proof machinery, not search: modern absorption and robust-expander decomposition techniques (the Bucić–Montgomery route), regularity-based dense-case arguments à la Conlon–Fox–Sudakov, or a Lean formalization of a new decomposition argument.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #184 (T. F. Bloom) | website |
| REF-02 | Bucić–Montgomery, Towards the Erdős–Gallai cycle decomposition conjecture (O(n log* n) bound) | arxiv |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.