The Erdős–Gallai cycle-decomposition conjecture
The Erdős–Gallai cycle-decomposition conjecture is the subject of a manuscript dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math). The conjecture asserts that the edges of every graph on n vertices can be partitioned into O(n) cycles and single edges. The manuscript claims a proof. A human paper claiming an independent proof was submitted to arXiv on the same day as the collection's first public commit, about fifteen hours earlier. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
The original result
- Claim. There is an absolute constant C > 0 such that, for every finite simple undirected graph G on n vertices, the edge set of G has a partition into at most Cn parts, each the edge set of a cycle or a single edge (Theorem 1.1). The manuscript also derives cycle-only consequences for Eulerian graphs (Corollary 1.2). Source: the manuscript A linear cycle-and-edge decomposition of every graph, dated 24 September 2026.
- Formalization, as described by the repository. The scope note lean/docs/181.md states that the formalized result gives one absolute constant C > 0 such that every finite simple graph on n vertices has an edge-disjoint decomposition into at most Cn cycles or singleton edges, including edgeless and small graphs, and that the optimal value of C is not determined. The Comparator statement is
CycleDecomposition.lean. - Dates. The repository's initial public commit,
adc7f12, is timestamped 6 October 2026, 21:58:50 UTC.
Earlier published results
- Erdős, Goodman and Pósa (1966) recorded the problem and an O(n log n) bound. Conlon, Fox and Sudakov improved the bound to O(n log log n) (2014), and Bucić and Montgomery to O(n log* n). Linear bounds were known for random graphs and for graphs of linear minimum degree. If cycles and edges may overlap, Pyber (1985) showed that n − 1 of them cover every graph. These citations follow the introduction of the OpenAI manuscript.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 15 October 2026) |
|---|---|---|---|---|
| 2026-10-06 (v1), 2026-10-09 (v2) | arXiv:2610.07840 (v1, v2), J. Kim; titled A proof of the Erdős–Gallai cycle decomposition conjecture | Independent proof (parallel) | Proves that the edges of every n-vertex graph can be decomposed into O(n) cycles and edges; equivalently, every Eulerian graph on n vertices decomposes into O(n) cycles, which the abstract describes as confirming Hajós' conjecture up to a constant factor. Version 1 was submitted on 6 October 2026 at 06:42:42 UTC. A "Note added" in v2 states that OpenAI announced an independent proof after v1 was submitted and before it appeared, and compares the strategies: the OpenAI proof is described as an induction on the number of vertices through pieces of large cut expansion and quotient graphs; Kim's proof finds near-closed subgraphs of polynomial minimum degree in light graphs, without expanders, and extends a result of Conlon, Fox and Sudakov from linear to polynomial minimum degree. Version 2 also simplifies the first version. The paper discloses extensive use of ChatGPT and Claude, and states that the author verified all results. | arXiv v2. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full": its note describes the formal statement as exactly the Erdős–Gallai conjecture with an absolute constant (parts are edge sets of Mathlib cycles or single edges, pairwise disjoint and covering the edge set). It records a sandboxed Comparator pass for the challenge CycleDecomposition (8 October 2026). |
The review states that "full" means the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked". |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.