Combinatorics·OpenAI Math·Result 181·Lean formalisation listed
The Erdős–Gallai cycle-decomposition conjecture
One of the 372 results in OpenAI's public mathematics catalogue, filed under combinatorics: 1 preprint, the latest dated 24 September 2026. This page quotes OpenAI's own summary of the claim, links the paper and abstract, and embeds the animation.
What OpenAI claims
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)
Paper
A linear cycle-and-edge decomposition of every graph
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.
Status
Preprint. The paper has not been independently reviewed. Treat the result as OpenAI's claim until other mathematicians have checked it. If a video exists, it illustrates the statement; it is not the proof.
The video
Erdős–Gallai Conjecture: Every Graph Splits Into Few Loops · Short · 0:21 · description, sources and transcript →
Related results in Combinatorics
- 182Power savings for intersective polynomial differences and prime argumentsLean
- 183Power savings for planar halving lines and k-setsLean
- 184Correspondence coloring with a fixed forbidden subgraphLean
- 185Counterexamples to infinite matroid intersection and packing/coveringLean
- 186Uniform influence and sharp thresholds for graph and hypergraph propertiesLean
- 187Snaky in 21 Maker movesLean
