Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 184
claims/: The 2 claim pages of Problem 184, one per claimant's result; the problem's standing derives from them.
Statement. Any graph on vertices can be decomposed into many edge-disjoint cycles and edges.
Formulation. The site's wording, read 2026-09-18 (page last edited 1 April 2026). A decomposition is a partition of the edge set into pieces, each a cycle or a single edge; the pieces are edge-disjoint, so this is the decomposition (packing) problem and not the covering problem, in which the cycles may share edges. Write for the least number such that every -vertex graph decomposes into at most cycles and edges ([CFS14], p. 609; the 1966 paper's counts edge-disjoint circuits with single edges counted as circuits, and [Er71] writes ). The statement asks whether . It is equivalent to asking whether every -vertex Eulerian graph decomposes into cycles ([BM22], p. 1, with the remark that the best constants in the two forms should differ). The constant is not part of the question: is known, so the cannot be replaced by , and the conjectured sharp constant is not fixed by the statement.
Status. OPEN, the site's label (page last edited 1 April 2026; proof-claim
tab read 2026-10-07); the derived standing of this page is solved, proved. The
two differ because the standing rests on a theorem the label does not reflect:
the site's page was last edited before either 2026 claim, and the release's
theorem below is not on the site's proof-claim tab. Theorem 1.1 of the OpenAI
mathematics release's preprint of 24 September 2026 gives an absolute with
for every . It is recorded on
its claim page
as accepted, with evidence formalized only: the corpus's verification of
2026-10-07 built the release's Lean declarations OAI.ErdosGallai.erdos_gallai,
MainStatement, EdgeDecomposition and CycleOrSingleEdge at the pinned
revision, found exactly the axioms propext, Classical.choice and
Quot.sound, and audited the formal statement for fidelity to the question, an
audit that belongs to that evidence and is not an outside review; no outside
reviewer is recorded, the informal manuscript is unrefereed and its proof was
read for structure only. A second full claim, Ryan Coffey's Lean-formalized
proof of the formal-conjectures statement (1 October 2026), is recorded as
claimed on
its claim page.
Before these, the best upper bound in the refereed record was
Bucić and Montgomery's Theorem 2,
with the iterated logarithm (Adv. Math. 437
(2024), refereed; cited from the arXiv v2), after Conlon, Fox and Sudakov's
(Random Structures Algorithms 45 (2014), refereed) and the
classical that the 1966 paper asserts; it remains the best refereed
bound. The lower bounds are from Gallai's graph
(1966) and from the complete bipartite graphs
, the construction Bucić and Montgomery give for Erdős's 1983
remark, so the constant is at least and is not determined. The
conjecture was known for the random graph and for graphs of linear
minimum degree (Conlon, Fox and Sudakov, Theorems 1.3 and 1.4). The search whose
scope the Current assessment records predates both claims and found neither a
proof nor a disproof.
Source. erdosproblems.com/184, accessed 2026-09-18: the problem page (OPEN, with the site's note that no finite computation can settle it; last edited 1 April 2026; source keys [EGP66], [Er71], [Er76], [Er81], [Er83b], with [BM22] and [CFS14] cited in the commentary), its one-comment discussion thread and its empty proof-claim tab. Cite as: T. F. Bloom, Erdős Problem #184, https://www.erdosproblems.com/184, accessed 2026-09-18.
References.
- [BM22] Bucić, M. and Montgomery, R., Towards the Erdős-Gallai cycle decomposition conjecture. arXiv:2211.07689 (v1 14 November 2022; v2 14 November 2023, "Final version, accepted for publication"); Adv. Math. 437 (2024), Paper No. 109434, doi:10.1016/j.aim.2023.109434 (Crossref record read; not held); extended abstract in Proceedings of the 55th Annual ACM Symposium on Theory of Computing (STOC 2023), 839--852, doi:10.1145/3564246.3585218. Conjecture 1, p. 1; Theorem 2, p. 2; Lemma 26 and the proof of Theorem 2, pp. 23--24; the lower bound, p. 24. Library home: bucic_2022_towards_erdos_gallai_cycle_decomposition_conjecture.
- [CFS14] Conlon, David and Fox, Jacob and Sudakov, Benny, Cycle packing. Random Structures Algorithms 45 (2014), no. 4, 608--626, doi:10.1002/rsa.20574 (received 2 October 2013, accepted 13 May 2014; cited in the journal's pagination); arXiv:1310.0632 (v2 22 May 2014; not held). Conjecture 1, Theorems 1.2--1.4 and the lower bounds, p. 609. Library home: conlon_2014_cycle_packing.
- [EGP66] Erdős, Paul and Goodman, A. W. and Pósa, Lajos, The representation of a graph by set intersections. Canadian J. Math. 18 (1966), 106--112; Section 5, p. 110. Library home: erdos_1966_representation_graph_set_intersections (a scan); the passage is paged at section_5.
- [Er71] Erdős, P., Some unsolved problems in graph theory and combinatorial analysis. Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97--109; item 11, pp. 101--102. Library home: erdos_1971_unsolved_problems_graph_theory_combinatorial_analysis; the passage is paged at item_11.
- [Er76] Erdős, Paul, Problems and results in combinatorial analysis.
Colloquio Internazionale sulle Teorie Combinatorie (Roma, 1973), Tomo II
(1976), 3--17; MR 0465878 (the site's reference text).
Library home:
erdos_1976_problems_results_combinatorial_analysis
(the Rényi archive's scan
1976-35.pdf, p. 15; the card carries the row for this problem). Cited by [BM22] (its [15]) among Erdős's collections that mention the conjecture. - [Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica 1 (1981), 25--42. Library home: erdos_1981_combinatorial_problems_which_i_would_most, a retyped copy without the journal's pagination; the passage is on its p. 8 (Part IV, item 3).
- [Er83b] Erdős, P., On some of my conjectures in number theory and
combinatorics. Proceedings of the fourteenth Southeastern conference on
combinatorics, graph theory and computing (Boca Raton, Fla., 1983), Congr.
Numer. 39 (1983), 3--19; MR 734525 (the site's reference text). Library home:
erdos_1983_some_my_conjectures_number_theory_combinatorics
(the Rényi archive's scan
1983-15.pdf, item 6, p. 15; the card carries the row for this problem). Cited by [BM22] (its [17]) as the source of the remark. - [Py85] Pyber, L., An Erdős--Gallai conjecture. Combinatorica 5 (1985), 67--79, doi:10.1007/BF02579444 (Crossref record). Not held and not cited by the site; the covering version, quoted on p. 2 of [BM22] and p. 609 of [CFS14].
- [GGKO21] Girão, A., Granet, B., Kühn, D. and Osthus, D., Path and cycle decompositions of dense graphs. J. London Math. Soc. (2) 104 (2021), 1085--1134, doi:10.1112/jlms.12455; arXiv:1911.05501 (arXiv record read). Not held; quoted on pp. 2 and 24 of [BM22].
- [AABC25] Akbari, S., Aloni, J., Beikmohammadi, A. and Clow, A., Tight bounds for cycle-edge decompositions and covers. arXiv:2509.01901 (v1 2 September 2025; v2 7 September 2025). Preprint, not held, abstract only; a lead.
Formalization. The release's Lean declaration
OAI.ErdosGallai.erdos_gallai was built by the corpus's verification at the
pinned revision, with the axioms propext, Classical.choice and
Quot.sound only, as the accepted claim page records, and Coffey's claim
page records his claimed Lean proof of erdos_184 itself. On the site's
side: statement only. The file
ErdosProblems/184.lean
of formal-conjectures, declares erdos_184 under category research open with proof sorry: there is a function such that
every finite simple graph has a decomposition into subgraphs, each a cycle or
a single edge (IsCycleOrEdge: connected and -regular, or with exactly
one edge), with at most parts. It carries five variants, all
sorry: n_log_n, lower_bound (the graph needs at least
parts), bucic_montgomery and conlon_fox_sudakov (minimum degree
gives parts) under research solved, and
covering under research open with answer(sorry), asking whether
cycles and edges whose edge sets cover the graph always exist. That covering
statement was proved by Pyber in 1985 according to [BM22] and [CFS14], so at
that commit the file's label and the literature differed; the
file at main, labels covering research solved with answer(True) and
cites Pyber [Py85] in its docstring (changed 30 September 2026), while
erdos_184 stays research open with no formal_proof attribute. The
community database (teorth/erdosproblems) records the
problem open (last changed 31 August 2025), the statement formalized since 16
March 2026 and no formal proof. Nothing was built.
Current assessment
The question (site formulation, accessed 2026-09-18). The statement above; OPEN, with the site's note that the problem is not decidable by a finite computation; last edited 1 April 2026. The commentary, in summary, attributes the conjecture to Erdős and Gallai and the bound to them as well, pointing to Section 5 of [EGP66]; notes that forces at least pieces; records Erdős's suggestion in [Er71] that pieces suffice when they need not be edge-disjoint; names Bucić and Montgomery's as the best bound and Conlon, Fox and Sudakov's for minimum degree at least ; and refers to Problems 583 (paths) and 1017 (complete graphs). The discussion thread has one comment (16 March 2026) locating the source of the proof in Section 5 of [EGP66], after which the site was updated. The proof-claim tab was empty on 2026-09-18; the one claim posted since is recorded below. The community database record says open.
Upper bounds. The chain is $O(n\log n)\to O(n\log\log n)\to O(n\log^\star n)$.
- : the 1966 paper writes, on p. 110, "It can be shown that ", with no proof (section_5); [Er71] says "We showed " (item_11). The argument is written on p. 609 of [CFS14]: by the Erdős--Gallai long-cycle theorem, greedily removing longest cycles halves the number of edges after cycles, and iterating gives . So the site's "who proved" rests on an assertion in the 1966 paper and a standard argument recorded later.
- : Theorem 1.2 of Conlon, Fox and Sudakov: every -vertex graph with average degree decomposes into cycles and edges. Acceptance evidence: Random Structures and Algorithms is refereed; the journal version (received 2 October 2013, accepted 13 May 2014, published online 16 October 2014) is the text cited. The statement (p. 609) is checked clause by clause; the proof (Sections 2--3) was not read.
- : Theorem 2 of Bucić and Montgomery: any -vertex graph decomposes into cycles and edges; the proof gives cycles and edges, and cycles and edges for any fixed (p. 24). Acceptance evidence: the arXiv v2 is described as the final version accepted for publication, and the Crossref record gives Advances in Mathematics 437 (2024), 109434, a refereed journal; the journal text was not compared. The statement (p. 2) is checked clause by clause; Lemma 26 and the deduction of Theorem 2 from it (pp. 23--24) were read for structure only. The authors write (p. 24) that the main bottleneck is the number of edges left uncovered in the almost decomposition into robust expanders, and that the iteration reduces the conjecture "to the case of arbitrarily sparse graphs". The release's 2026 theorem, recorded under Resolution below, removes the .
Lower bounds. Gallai's graph (the 1966 paper's ) needs edge-disjoint circuits when , so (p. 110); the site's "" is the weaker form in which [Er71] states the same example (" shows that "). The best lower bound is , which [BM22] (p. 1) and [CFS14] (p. 609) attribute to a remark of Erdős in 1983 ([Er83b] p. 15: "An example of shows that ", naming no graph); Bucić and Montgomery give the construction they take it to refer to (lower_bound_p24): needs at least cycles and edges, since each of the vertices of odd degree forces a single edge and every cycle has length at most ; with this is Gallai's . Conversely, Hajós's conjecture (every Eulerian graph on vertices decomposes into at most cycles) would give (p. 24), so is the expected constant; the problem's asks less.
Special classes where the conjecture holds. Theorem 1.3 of Conlon, Fox and Sudakov: for an absolute and every , decomposes a.a.s. into at most cycles and edges; Theorem 1.4: minimum degree gives , the site's "". The sharper results Bucić and Montgomery report on p. 2, Korándi, Krivelevich and Sudakov's constant for , Glock, Kühn and Osthus's exact count for constant , and [GGKO21]'s for large graphs of linear minimum degree, are second-hand; none of those papers is held.
The covering variant, not the problem. The 1966 paper (p. 110) and [Er71] (p. 102) ask whether circuits, not required to be edge-disjoint, always cover the edges. This is the covering version, and it is proved: Pyber showed in 1985 that the edges of any -vertex graph can be covered with cycles and edges ([Py85], quoted on p. 2 of [BM22] and p. 609 of [CFS14]; not held). The analogous covering version of Gallai's path conjecture (Problem 583) was proved by Fan in 2002, as the same pages record. Neither covering theorem bears on the decomposition question.
Erdős's statements. The 1966 paper defines , proves the bound from Gallai's oral communication, asserts and writes "it may be true that for some suitable " (p. 110). The 1971 list, item 11 (pp. 101--102), states the same three points for and adds the covering variant. The 1981 Combinatorica paper says, on p. 8 of the retyped copy (Part IV, item 3): "Gallai and I conjectured that the edges of every can be covered by edge disjoint circuits or edges of our . We easily showed that the result holds with replacing ." The Rome 1973 paper ([Er76], p. 15) states it as "Gallai and I conjectured that every can be covered by at most edge disjoint circuits and edges. We could only prove this with instead of ." The 1983 Boca Raton paper ([Er83b], p. 15, item 6) states both forms, the covering conjecture first and the decomposition conjecture second: "Gallai and I conjectured that the edges of every can be covered by at most circuits and edges of . We also conjectured that there is an absolute constant so that the edges can be covered by at most edge disjoint circuits and edges of . An example of shows that ." It reports that Pyber had proved the first conjecture a few months earlier using a result of Lovász, and that the second remains open and may need new ideas. Bucić and Montgomery cite both among the collections in which Erdős mentioned the conjecture, and the second as the source of the remark.
A recent preprint on special classes. The arXiv API search returned [AABC25] (September 2025), whose abstract states that every graph with maximum degree at most decomposes into at most cycles and edges, that every -vertex claw-free graph decomposes into at most -regular subgraphs and edges, and that every graph containing a cycle can be covered by at most cycles and edges, improving Pyber's covering theorem; the abstract calls Bucić and Montgomery's bound the best upper bound and repeats the lower bound. The preprint was not read beyond its abstract, is not held and is not refereed as far as found; a special class, not the general problem.
Resolution (2026). Two full claims postdate the search below.
- The OpenAI mathematics release's preprint A linear cycle-and-edge
decomposition of every graph (24 September 2026) states as its Theorem 1.1
that for an absolute the edges of every simple graph on vertices
split into at most classes, each the edge set of a simple cycle or a
single edge, with fixed last in the proof and not made explicit; its
Corollary 1.2 is the Eulerian form. The manuscript is carded at
its card,
with
Theorem 1.1
and
Corollary 1.2
paged at claims checked and the proof read for structure only. The release's
Lean tree proves the theorem as
OAI.ErdosGallai.erdos_gallai, pinned by the comparator challengeCycleDecomposition.lean; the corpus's verification of 2026-10-07 built it at the pinned revision, found exactly the three standard axioms and audited the formal statement for fidelity, the formalized evidence, and the only kind, recorded on the claim page. The derived standing of this page follows from it. The informal proof is unrefereed and not independently reviewed. - Ryan Coffey's paper A proof of the Erdős–Gallai cycle decomposition
conjecture and Lean 4 repository (first public commit and forum posting
2026-10-01) prove the formal-conjectures statement
Erdos184.erdos_184unchanged, by the author's account with only the three standard axioms, keeping the Bucić--Montgomery round structure and removing its per-round cost; the site's tab names Claude Opus 5.5 as the AI system used. The corpus has not built the development; claims checked on the README, the pinned statement and the forum entry, with the paper and the proof not checked; it is recorded as claimed on its claim page.
Search scope. The search predates both claims under Resolution; none of the routes below found a proof of , a disproof, or a proof claim.
- The site: problem page, discussion thread and proof-claim tab as read
2026-09-18; the community database record; formal-conjectures
184.leanat the pinned commit; the site's reference pages for the keys [Er76] and [Er83b] (their texts are not in the problem page). - arXiv: the API records of 2211.07689 (v2, final accepted version) and
1310.0632 (v2 of 22 May 2014); the search
abs:"Gallai" AND abs:"cycles and edges"sorted by date (five records: [AABC25], [BM22], [GGKO21], Korándi--Krivelevich--Sudakov's random-graph paper, [CFS14]). The API searches titles and abstracts only, so this zero for newer general bounds is weak. - Crossref: the records of doi:10.1016/j.aim.2023.109434 and doi:10.1002/rsa.20574, and a bibliographic query on the title of [BM22] (which also returned the STOC 2023 proceedings article and Pyber's 1985 Combinatorica paper).
- Semantic Scholar: the citation list of [BM22] was requested twice and answered HTTP 429 both times; not obtained.
- The primary sources at the pages stated above: [BM22] pp. 1--2, 23--24; [CFS14] pp. 608--609; [EGP66] pp. 109--110; [Er71] pp. 101--102; [Er81] p. 8 of the copy; [Er76] p. 15; [Er83b] p. 15.
Not searched: MathSciNet, zbMATH, Google Scholar, X. Not held: [Py85], [GGKO21], [AABC25], Lovász 1968, Korándi--Krivelevich--Sudakov, Glock--Kühn--Osthus, the journal texts of [BM22].
Remaining gaps. (1) Proof coverage is statements only: Theorem 2 of
[BM22] and Theorems 1.2--1.4 of [CFS14] are paged at claims checked, Lemma 26
and Section 5.6 of [BM22] read for structure; the release's Theorem 1.1 is
paged at claims checked with its proof read for structure; what is checked is
the release's formal statement and kernel-checked proof, by the corpus's own
build and audit and by no outside reviewer, not any informal argument, and
no refereed version of either 2026 claim exists. The constant
is not determined (between and an unspecified value). (2) The
journal version of [BM22] was not compared with the arXiv v2.
(3) The 1983 remark behind the bound names no graph, so
the construction is Bucić and Montgomery's reading of it. (4) The 1966
upper bound is
asserted, not proved, in the paper; the argument is recorded from [CFS14].
(5) The formal-conjectures covering variant was labeled open at the
commit read although Pyber's theorem answers it; the file at
main labeled it solved as recorded above.
Proof claims on the site. The site's proof-claim tab carries one claim, full: Ryan Coffey's paper and Lean formalization of 2026-10-01, described under Resolution above and recorded on its claim page as claimed. The release's theorem is not on the site's tab. The site labels the problem OPEN (page last edited 1 April 2026); this page's standing is derived from the claim pages, not from the label.
Known results
- OpenAI 2026, Theorem 1.1 (accepted on the formal proof; unrefereed): for an absolute , the problem's answer; Coffey 2026 (claimed): a second Lean-formalized proof of .
- Bucić--Montgomery, Theorem 2 (2023; Adv. Math. 2024): , the best refereed upper bound; Conjecture 1 states the problem; the Section 6 construction gives .
- Conlon--Fox--Sudakov, Theorem 1.2 (2014): for average degree ; Theorem 1.3: a.a.s. into pieces; Theorem 1.4: minimum degree into pieces.
- Erdős--Goodman--Pósa, Section 5 (1966): the conjecture , , the asserted .
- Erdős 1971, item 11: , probably , , and the covering variant later proved by Pyber (1985, not held).
Linked library material
These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.
- bucic_2022_towards_erdos_gallai_cycle_decomposition_conjecture
- bucic_2022_towards_erdos_gallai_cycle_decomposition_conjecture / conjecture_1
- bucic_2022_towards_erdos_gallai_cycle_decomposition_conjecture / lower_bound_p24
- bucic_2022_towards_erdos_gallai_cycle_decomposition_conjecture / theorem_2
- conlon_2014_cycle_packing
- conlon_2014_cycle_packing / theorem_1_2
- conlon_2014_cycle_packing / theorem_1_3
- conlon_2014_cycle_packing / theorem_1_4
- erdos_1959_maximal_paths_circuits_graphs
- erdos_1959_maximal_paths_circuits_graphs / theorem_2_7
- erdos_1966_representation_graph_set_intersections
- erdos_1966_representation_graph_set_intersections / section_5
- erdos_1966_representation_graph_set_intersections / theorem_4
- erdos_1971_unsolved_problems_graph_theory_combinatorial_analysis
- erdos_1971_unsolved_problems_graph_theory_combinatorial_analysis / item_11
- erdos_1976_problems_results_combinatorial_analysis
- erdos_1976_problems_results_combinatorial_analysis / conjecture_p15
- erdos_1983_some_my_conjectures_number_theory_combinatorics
- erdos_1983_some_my_conjectures_number_theory_combinatorics / conjecture_p15
- openai_2026_linear_cycle_edge_decomposition_graph
- openai_2026_linear_cycle_edge_decomposition_graph / corollary_1_2
- openai_2026_linear_cycle_edge_decomposition_graph / theorem_1_1
- erdos_1981_combinatorial_problems_which_i_would_most