---

Claim. There is an absolute constant $C>0$ such that, for every $n$, the edge set of every simple graph on $n$ vertices has a partition into at most $Cn$ parts, each the edge set of a simple cycle of the graph or a single edge of it. In the notation of Problem 184, $f(n)\le Cn$ for every $n$, so $f(n)=O(n)$ and the problem's question is answered yes. This is Theorem 1.1 of OpenAI, A linear cycle-and-edge decomposition of every graph, a preprint of the OpenAI mathematics release dated 24 September 2026 (the claim's date), carded in the library at its card and stated on its result page; its Corollary 1.2 gives the Eulerian form (every graph with all degrees even partitions into at most $Cn$ cycles). The manuscript places itself after the $O(n\log n)$ of Erdős and Gallai, the $O(n\log\log n)$ of Conlon, Fox and Sudakov and the $O(n\log^\star n)$ of Bucić and Montgomery, and builds on the last paper's expansion and routing method through a multiscale induction; the constant $C$ is fixed last in the proof and is not made explicit. The order is sharp: trees need $n-1$ parts and complete bipartite graphs force $(\tfrac32-o(1))n$, as the problem page records.

Depends on. Nothing in this wiki. The manuscript proves its lemmas itself, adapting and reproving lemmas of Bucić and Montgomery and of Conlon, Fox and Sudakov; its external theorem inputs are Lovász (1968), Theorem 1, and the Aharoni--Haxell theorem in the form of Bucić and Montgomery's Theorem 6, and the second part of Corollary 1.2 also cites Girão, Granet, Kühn and Osthus.

Acceptance. Formalized only. The release's Lean tree (the lean/ folder at the pinned revision linked above) declares, in the namespace OAI.ErdosGallai, the definitions CycleOrSingleEdge (a set of edges that is the edge set of a cycle walk of $G$ or a single edge of $G$) and EdgeDecomposition (a family of $k$ such sets, pairwise disjoint, with union the edge set of $G$), the proposition MainStatement (some real $C>0$ such that for every $n$ and every SimpleGraph (Fin n) there is $k\le Cn$ with an EdgeDecomposition into $k$ parts) and the theorem erdos_gallai : MainStatement. The comparator challenge lean/ComparatorChallenges/CycleDecomposition.lean pins the statement: it states these declarations with the theorem left open, and the solution module of the release proves it. The corpus's verification of 2026-10-07 built the declarations from the release's tree at the pinned revision, printed the axioms of erdos_gallai and found exactly propext, Classical.choice and Quot.sound, compared the challenge text with the solution's copies of the statement and found them identical in the same namespace with the same opens, and audited the whole formal statement for fidelity, the statement audit that formalized requires and the corpus's own work, not an outside review: in the pinned Mathlib a cycle walk is a closed trail without repeated vertices, so each part is a simple cycle of length at least three or one edge; the parts are nonempty and disjoint, so $k$ counts the pieces; the constant is chosen before $n$ and the graph, so it is absolute; and no definition in the import chain redefines a name the statement uses. The audit found no hidden hypothesis or trivializing reading. One $C$ for all $n$ is the problem's $f(n)=O(n)$, since small orders are covered by single edges either way, and simple cycles are the strictest reading of the problem's "cycles". That audit concerns the formal statement and the kernel-checked proof. Not reviewed: no outside reviewer or documented independent acceptance is recorded, and the corpus's own verification record counts as neither. Not refereed: the informal manuscript's proof (Sections 2--7) was read for structure only, and no refereed publication, arXiv version or outside review of either is known. The release's own README says that its manuscripts were produced by an internal OpenAI model and are at different stages of verification, not all with Lean formalizations.

Relation to other statements. The formal-conjectures file 184.lean states the problem as Erdos184.erdos_184, with a function $f=O(n)$ and decompositions into subgraphs that are connected and $2$-regular or have one edge; the release's statement is a different formalization of the same question, and no Lean bridge between the two has been built. A second full claim, a Lean proof of the formal-conjectures statement itself, is recorded on its own claim page as claimed.