A published paper or arXiv preprint answers the main question of Erdős Problem #184 (theorem erdos_184 in formal-conjectures) in full (proof, disproof, or the exact value asked for) with no hypotheses beyond the problem's own.

The problem, as stated in formal-conjectures (Apache 2.0):

Any graph on n vertices can be decomposed into O(n) many edge-disjoint cycles and edges. This was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof.

References formal-conjectures lists for this problem (a starting point, not evidence):

• [BM22] Bucić, M. and Montgomery, R., Towards the Erdős-Gallai Cycle Decomposition Conjecture. arXiv:2211.07689 (2022).
• [CFS14] Conlon, David and Fox, Jacob and Sudakov, Benny, Cycle packing. Random Structures Algorithms (2014), 608-626.
• [EGP66] Erdős, Paul and Goodman, A. W. and Pósa, Lajos, The representation of a graph by set intersections. Canadian J. Math. (1966), 106-112.
• [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.
• [OAI26a] OpenAI, A linear cycle-and-edge decomposition of every graph. OpenAI Math Release preprint (2026).
• [Py85] Pyber, L., An Erdős-Gallai conjecture. Combinatorica (1985), 67-79.