Erdős Problem #184

OPENdatabase updated 2025-08-31

No proof or disproof is known, and it isn't known whether a finite computation could settle it.

What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).

A graph \(H\) is a cycle or an edge if it is connected and 2-regular, or if it has exactly one edge.

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.

Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 5 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/184.

Newer public claim (6 Oct 2026): OpenAI's internal-model release claims, for this problem, every graph decomposes into O(n) cycles and edges (Erdős–Gallai) — one of three claimed proofs within six days (Coffey 1 Oct with Lean of Formal Conjectures' statement, Kim 6 Oct on arXiv); refereed here 20 Oct; its Lean kernel-replayed on our machine 20 Oct and bridged to a verbatim copy of Formal Conjectures' statement — see /day/184-erdos-gallai-three-proofs-two-lean-replays-and-a-bridge — family 181 at github.com/openai/math, OpenAI's own Lean proves its MainStatement (∃ C > 0, every graph on Fin n has a cycle-and-edge partition into ≤ C·n parts) — kernel-replayed on our machine on 20 Oct 2026 (34 modules, standard axioms, statement identical to the comparator challenge, leanchecker --fresh over the whole closure rc 0); Formal Conjectures' erdos_184 is a different (equivalent) statement, a verbatim copy of which we derived from it in a kernel-checked bridge; Coffey's separate Lean proof of erdos_184 itself also replayed — see our /day entry. Bloom calls these claims, not endorsements.

Prizenone

Topicsgraph theory, cycles

Statement in LeanFormal Conjectures

Solution in Leanno

Original pageerdosproblems.com/184

Attempts

submit one →

FULL WRITE-UP BY THIS SITE · OCT 20, 2026

Read our full write-up →

Erdős and Gallai conjectured that every n-vertex graph is the edge-disjoint union of O(n) cycles and single edges; the record at the end of September was Bucić–Montgomery's O(n log* n). Three claimed proofs of the full conjecture then appeared: Ryan Coffey's (public 1 October with a 152-page paper and a Lean proof of Formal Conjectures' exact statement), Jaehoon Kim's (arXiv, 6 October, 22 pages in v2, no Lean) and OpenAI's (released 6 October, 32 pages, with a Lean proof of its own formulation). We compiled both Lean proofs on our machine: each depends only on the three standard axioms, leanchecker --fresh accepts each whole import closure, wrong-shape controls are rejected and planted-sorry controls show sorryAx. Formal Conjectures marks the problem solved with a link to OpenAI's proof, which proves an equivalent but different statement; we wrote the transport and kernel-checked it against a verbatim copy of Formal Conjectures' statement, while Coffey's proof is checked against Formal Conjectures' own. Hostile AI referee seats found no gap in the parts they checked: OpenAI's paper (expository fixes), Coffey's load-bearing chain (his §3–§5 device lemmas only at statement level; the Lean carries them) and Kim's v2, read line by line (nothing above exposition; the cited Bucić–Montgomery results not re-proved). No independent human check of any of the three is on record.

CLOSED

← #183 the board #185 →