Proves that the edges of every finite simple undirected graph on n vertices can be partitioned into at most Cn simple cycles and single edges, for an absolute constant C. This resolves the Erdős–Gallai cycle-decomposition conjecture, bounding the number of pieces linearly even for dense graphs. (Lean)
Manuscript
A linear cycle-and-edge decomposition of every graph
September 24, 2026 · source · Lean formalization available · cite as \cite{OAI:A-linear-cycle-and-edge-decomposition-of-every-graph-September-24-2026}
We prove that every finite simple undirected graph on n vertices has an edge partition into at most Cn simple cycles and single edges, for an absolute constant C. This resolves the Erdős–Gallai cycle decomposition conjecture positively.
Result 181 · Combinatorics. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.
Source: https://github.com/openai/math/blob/main/CONTENTS.md