Proposed
Separately authored proof manuscript ↗
The same universal cycle double cover question.
An independent proof of the Cycle Double Cover Conjecture · Abstract and theorem statement →
Observed Oct 13, 2026
Conjecture · version 1
Every bridgeless graph has a cycle double cover
Earlier version 1. View current version 2 →
Statement
For every finite loopless undirected multigraph G with no bridges, there exists a multiset C of cycles in G such that every edge of G belongs to exactly two members of C, counted with multiplicity.
Assumptions
- Finite undirected multigraph.
- No loops and no bridges.
- Parallel edges and repeated cycles in the cover are allowed.
Scope
Universal existence. The cited 2026 proof and formal endpoint are reported by their sources; independent mathematical assessment is pending.
Evidence
Source reports
Proposed
Full cycle double cover proof reported ↗
Universal finite loopless bridgeless multigraph formulation.
A proof of the cycle double cover conjecture · Main theorem and flow-to-cover construction →
Observed Oct 13, 2026
Proposed
Unconditional Lean endpoint reported complete ↗
CDCLean.cycleDoubleCover_of_bridgeless, with no additional project axioms reported.
Cycle double cover in Lean · CDCLean/Main.lean; README verification and exact endpoint →
Observed Oct 13, 2026
Formal proofs
Lean: the full bridgeless multigraph statement ↗
Complete formal proof reported externally
The project reports an unconditional proof endpoint using only standard logical axioms. It is linked as source evidence while mathematical assessment of the new proof remains pending.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Declaration & revision
CDCLean.cycleDoubleCover_of_bridgelessCommit 577e9d9ea326d520f80672ee69b830bf1d513df5
Connections
In this problem · publication v1
Cycle double cover conjecture →
Primary formulation · Proposed
Relationship not independently reviewed. This concerns its use in this problem.
Sources
A proof of the cycle double cover conjecture →
- Main theorem and flow-to-cover construction → · Original passage ↗
Recorded wording
A new argument is reported to construct a cycle double cover for every finite loopless bridgeless multigraph.
paraphrase · OpenMath supplies original paraphrases and links; no proof text is republished.
OpenAI · Preprint · Publication date Jul 10, 2026
Public manuscript or exposition; publication does not imply independent OpenMath review.
Revision & attribution
Source revision: 2026-07-10. Observed Oct 13, 2026.
OpenAI reports a GPT-5.6 Sol Ultra multi-agent discovery workflow. This provenance is first-party and is not independent mathematical review.
Source updated Jul 10, 2026.
An independent proof of the Cycle Double Cover Conjecture →
- Abstract and theorem statement → · Original passage ↗
Recorded wording
A separately authored manuscript reports a proof of cycle double cover using an AI-assisted workflow.
paraphrase · OpenMath supplies original paraphrases and links; no proof text is republished.
Shiva Kintali · Preprint · Publication date Jul 2026
Public manuscript or exposition; publication does not imply independent OpenMath review.
Revision & attribution
Source revision: 2026-07. Observed Oct 13, 2026.
Shiva Kintali reports work with Codex; this is a distinct manuscript and has not been adjudicated by OpenMath.
Cycle double cover in Lean →
- CDCLean/Main.lean; README verification and exact endpoint → · Original passage ↗
Recorded wording
The source endpoint covers finite loopless bridgeless multigraphs via a formalized eight-flow theorem and a conversion to cycle covers.
paraphrase · OpenMath supplies original paraphrases and links; no proof text is republished.
OpenAI · openai/cdc-lean project · Project documentation · Publication date Jul 9, 2026
Public formal source; build and independent mathematical review are separate checks.
Cycle double cover in Lean — pinned source ↗No OpenMath execution recorded
Public source inspected for statement and assumptions; this proof project has not been executed by OpenMath.
Revision & attribution
Source revision: 577e9d9ea326d520f80672ee69b830bf1d513df5. Observed Oct 13, 2026.
This formal source accompanies the OpenAI AI-assisted proof report; formal checking and human exposition are separate evidence roles.
Source updated Jul 9, 2026.
Cycle double cover in Lean — pinned source: 577e9d9ea326d520f80672ee69b830bf1d513df5.
History
Statement versions
Statement versions and problem publication versions are separate. A new publication can update context or sources while retaining the same statement.
Assessment history · 3
Assessments retained in these publication records. Earlier statement versions retain their own source histories.
Proposed
Unconditional Lean endpoint reported complete ↗
CDCLean.cycleDoubleCover_of_bridgeless, with no additional project axioms reported.
Observed Oct 13, 2026 · Source passage →
Proposed
Full cycle double cover proof reported ↗
Universal finite loopless bridgeless multigraph formulation.
Observed Oct 13, 2026 · Source passage →
Proposed
Separately authored proof manuscript ↗
The same universal cycle double cover question.
Observed Oct 13, 2026 · Source passage →
Record details
- Claim ID
- claim-cycle-double-cover-existence
- Statement version
- 1
- SHA-256
- c54b91badb43914c11c9db1707643586ea66b63078c80e65945673e7e4d06637