https://openai-aftermath.mathnt.net/index.php?action=history&feed=atom&title=The_Erd%C5%91s%E2%80%93Gallai_cycle-decomposition_conjectureThe Erdős–Gallai cycle-decomposition conjecture - Revision history2026-10-15T06:49:30ZRevision history for this page on the wikiMediaWiki 1.46.2https://openai-aftermath.mathnt.net/index.php?title=The_Erd%C5%91s%E2%80%93Gallai_cycle-decomposition_conjecture&diff=96&oldid=prevAftermath bot: New page: the Erdos-Gallai cycle-decomposition conjecture, with J. Kim's independent proof and MathVet review2026-10-15T01:47:03Z<p>New page: the Erdos-Gallai cycle-decomposition conjecture, with J. Kim's independent proof and MathVet review</p>
<p><b>New page</b></p><div>'''The Erdős–Gallai cycle-decomposition conjecture''' is the subject of a manuscript dated 24 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math 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.<br />
<br />
== The original result ==<br />
* '''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 [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-linear-cycle-and-edge-decomposition-of-every-graph-September-24-2026 A linear cycle-and-edge decomposition of every graph], dated 24 September 2026.<br />
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/181.md 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 [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/CycleDecomposition.lean <code>CycleDecomposition.lean</code>].<br />
* '''Dates.''' The repository's initial public commit, [https://github.com/openai/math/commit/adc7f1241b42e322a6451854ab7e4b4c146bf78a <code>adc7f12</code>], is timestamped 6 October 2026, 21:58:50 UTC.<br />
<br />
== Earlier published results ==<br />
* 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.<br />
<br />
== Public follow-up work ==<br />
{| class="wikitable"<br />
! Date !! Work !! Relation !! Public claim !! Public status (checked 15 October 2026)<br />
|-<br />
| 2026-10-06 (v1), 2026-10-09 (v2) || [https://arxiv.org/abs/2610.07840 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.<br />
|-<br />
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 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 <code>CycleDecomposition</code> (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".<br />
|}<br />
<br />
== Notes ==<br />
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.<br />
<br />
[[Category:OpenAI results]]</div>Aftermath bot