Browse › Combinatorics › 181 The Erdős–Gallai cycle-decomposition conjecture
A linear cycle-and-edge decomposition of every graph
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
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.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Follow-up works
- Jaehoon Kim, A proof of the Erdős–Gallai cycle decomposition conjecture (arXiv:2610.07840, v1 6 Oct 2026, v2 9 Oct 2026). Contemporaneous independent proof of the same linear bound, developed with disclosed ChatGPT and Claude assistance; a v2 note acknowledges the OpenAI proof and contrasts its quotient-and-lifting induction with Kim's approach through light graphs and polynomial minimum degree.
- Ryan Coffey, proof claim for Erdős Problem #184 on the erdosproblems.com forum (forum post, 1 Oct 2026). Separate claimed proof of the $O(n)$ bound, listed as made with Claude Opus 5.5 and building on the Bucić–Montgomery round structure, posted after this preprint's date and before the release. [AI-generated per source]
Comments and discussion
- Thomas Bloom (erdosproblems.com), Erdős problems in the OpenAI proofs (blog post, 8 Oct 2026). The curator of the Erdős problems site lists this preprint under Problem 184, summarizes its claim and notes that "This proof has been formalised"; a comment in the thread points to the Coffey and Kim claimed solutions.
Formalization
- OpenAI, The Erdős–Gallai cycle-decomposition conjecture: Lean scope note (OpenAI Math Release, lean/docs/181.md, 2026-10-06). The release's scope note: it formalizes one absolute constant $C>0$ with at most $Cn$ cycles or single edges for every finite simple graph, including edgeless and small graphs, and leaves the optimal $C$ undetermined.
- OpenAI, lean/OAI/Combinatorics/CycleDecomposition/Main.lean (openai/math, commit adc7f12). Lean proof of
OAI.ErdosGallai.erdos_gallai, which proves theMainStatementfrom the comparator file ComparatorChallenges/CycleDecomposition.lean via an intermediate bound with the paper's inductive factor φ(n). - Google DeepMind formal-conjectures, FormalConjectures/ErdosProblems/184.lean (formal-conjectures, main branch). Independent formal statement
erdos_184, marked research solved, whose docstring credits this preprint and links to the OpenAI Lean proof. - Ryan Coffey, erdos-gallai-lean (GitHub, release tag 2026-10-01). Separate Claude-assisted Lean 4 formalization of a different proof (Coffey's) of the same theorem, targeting
Erdos184.erdos_184directly, with a manuscript, verification records and a trust-model discussion; it does not mention the OpenAI paper and its README states that "Nobody has checked the mathematics".
Related prior literature mentioned by others
- Matija Bucić and Richard Montgomery, Towards the Erdős–Gallai Cycle Decomposition Conjecture (arXiv:2211.07689; Advances in Mathematics 437, 109434, 2024). Kim's paper and the Erdős Problem a Day comparison identify this earlier $O(n\log^* n)$ result and its expander methods as background to the linear-bound proofs; it is also in the paper's bibliography.
- Richard Montgomery, Recent progress in graph theory using expansion (arXiv:2607.26049, 2026-07-28; ICM survey). Coffey's repository recommends this survey as context for the expansion methods underlying progress on the cycle-decomposition conjecture.
Possibly relevant literature (found by the agent, not checked)
- Richard Montgomery, Cycles and expansion in graphs (EMS Magazine 138, 2025, doi:10.4171/MAG/287). Expository survey of expansion-based methods for cycle problems, including the Erdős–Gallai problem and the Bucić–Montgomery sublinear-expansion approach that the paper says it builds on.
Digests and expositions
- Open Mathematics Courses / Claude Opus 5.5, The Erdős–Gallai cycle decomposition theorem (online course, undated). Eight lessons explain this manuscript's routing, reservoirs, pair folding, cycle lifting and final induction, with exercises and solutions; the source states that independent review is incomplete. [AI-generated per source]
News and blogs
- Patrick White with Claude, Erdős Problem a Day, Erdős #184: three claimed proofs, two Lean replays and a bridge (2026-10-20). Comparison of the OpenAI, Coffey and Kim proofs that reports local Lean kernel replays and a bridge from OpenAI's theorem to a copied Formal Conjectures statement, and labels its manuscript assessments as AI reviews rather than human referee verdicts. [AI-generated per source]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 181
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:A-linear-cycle-and-edge-decomposition-of-every-graph-September-24-2026,
author = {{OpenAI}},
title = {{A linear cycle-and-edge decomposition of every graph}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/A-linear-cycle-and-edge-decomposition-of-every-graph-September-24-2026/main.pdf}{OAI:A-linear-cycle-and-edge-decomposition-of-every-graph-September-24-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/181.md. The Lean statements have not been checked by people against the paper's claims.
Family 181: The Erdős–Gallai cycle-decomposition conjecture
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.
This is the only paper in this family.