---

Claim. Every graph on $n$ vertices decomposes into $O(n)$ edge-disjoint cycles and single edges, the statement of Problem 184, proved in the paper A proof of the Erdős–Gallai cycle decomposition conjecture by Ryan Coffey and formalized in the Lean 4 repository steelwheel01/erdos-gallai-lean, whose first public commit and whose posting to the site's proof-claim tab are both dated 2026-10-01 (the claim's date; the pinned commit is the repository's third). By its README, the repository proves the theorem Erdos184.erdos_184 of formal-conjectures, taken unchanged from that project's file FormalConjectures/ErdosProblems/184.lean at its commit of 2026-09-24: a function $f=O(n)$ such that every finite simple graph has a finite family of subgraphs, each connected and $2$-regular or with exactly one edge, with pairwise disjoint edge sets covering the graph and at most $f(|V|)$ members; the proof takes $f(n)=cn$ with a natural number $c$ that is not computed. The README reports that the proof uses exactly the axioms propext, Classical.choice and Quot.sound, no sorryAx and no project axiom, checked in a public release run by a comparator against the pinned upstream statement and by kernel replays, and it states that no human has reviewed the fidelity of the upstream statement to the conjecture for this project. The claim's summary on the site's tab describes the method in outline: the argument follows the Bucić--Montgomery scheme of rounds, in each of which the graph is split into robust sublinear expanders whose edges are mostly packed into cycles, and makes each round cost only a linear number of pieces, where the earlier proof paid for the $\log^\star n$ factor. Three devices are named: a decomposition chosen so that no vertex gathers too many edges over the rounds, a reserve of random edges that one round passes to later ones so that their cycles can be closed, and a set of reserved edges that gather the odd-degree remainders of all rounds into auxiliary graphs with at most $n/4$ vertices in all, whose decompositions are pulled back to the original graph and give a linear bound by induction. The site's tab names Claude Opus 5.5 as the AI system used, and the repository's disclosure credits an AI assistant.

Submission note. Posted to erdosproblems.com as a proof claim by Ryan Coffey (account American-Pharaoh) on 1 October 2026, giving "Claude Opus 5.5" as the AI used:

We prove the Erdős–Gallai conjecture (Erdős #184), improving the previous O(n log* n) bound of Bucić and Montgomery to O(n). The proof keeps their round structure — repeatedly decompose into robust sublinear expanders and cover most of each by cycles — but removes the per-round cost behind the log* n. Three new ingredients do this: a modified expander decomposition that stops any vertex from concentrating edges across rounds; expanders that lend random edges to later rounds so those rounds can close their edges into cycles; and private junction edges that route the odd leftovers of all rounds into small quotient graphs with at most n/4 vertices in total, whose decompositions lift back to the original graph, so induction gives f(G) ≤ C₀n + 2c·(n/4) ≤ cn. The proof is formally verified in Lean 4 against the formal-conjectures statement.

Depends on. Nothing in this wiki; the formal-conjectures statement it proves is the one the problem page's Formalization section records.

Standing. Claimed. The corpus has not built, replayed or audited the development: claims checked on the README, the pinned statement text and the forum entry; the paper and the proof were not checked, and no outside review is known. The author's own verification record is the repository's and is not a documented independent acceptance; the site labels the problem OPEN (proof-claim thread read 2026-10-07). The problem's standing rests on the accepted release theorem recorded on OpenAI's claim page, which this claim would independently confirm if accepted.