openmath.dev
Esc

Loading…

↑ ↓ to move↵ to open

Appearance
Appearance
← Problems

Combinatorics · Conjecture

Cycle double cover conjecture

Does every finite bridgeless loopless multigraph admit a collection of cycles that covers each edge exactly twice?

ProposedOpenMath assessment · Oct 13, 2026
Frontier 1 report →
Cite & export
Open this versionExport record · JSONRecord detailsReport a correction
Use with an agent

Earlier version 5 of this page. View current →

Overview

Current assessment

A full proof and an unconditional Lean endpoint are reported in the selected 2026 sources. OpenMath presents them as a proposed resolution pending independent mathematical assessment.

Open questions

The universal bridgeless multigraph target and stronger variants must retain their separate scopes.

Latest

Precise statement

Undirected finite multigraphs: parallel edges are allowed, loops are excluded, and a bridge is an edge whose deletion increases the number of connected components. The cover is a multiset of cycles; the same cycle may occur twice. Two parallel edges may form a cycle.

Definitions

Bridgeless graph
A graph with no edge whose removal increases the number of connected components. Every edge must occur twice in the requested collection of cycles.

Background

How to read this question

Stronger covering questions need their own statements

The ordinary statement imposes no fixed small number of even subgraphs or coloring constraints. A reported proof does not automatically resolve stronger covering or coloring conjectures.

Limit No stronger five-cover or coloring result is assessed by this page.

Sources & review

Supporting statements

Source-grounded explanation · independent explanation review: pending.

Question paraphrased by OpenMath. Original wording is available in the sources.

Landscape

Figures and explorable examples. Selecting a statement opens its exact wording.

A cycle double cover of the Petersen graph

Each panel highlights one cycle of the cover; every edge is highlighted in exactly two panels.

0123456789
The Petersen graph
0123456789
Cycle 1: 0 – 1 – 2 – 3 – 4 – 0
0123456789
Cycle 2: 0 – 1 – 6 – 8 – 5 – 0
0123456789
Cycle 3: 0 – 4 – 9 – 7 – 5 – 0
0123456789
Cycle 4: 2 – 3 – 8 – 6 – 9 – 7 – 2
0123456789
Cycle 5: 1 – 2 – 7 – 5 – 8 – 3 – 4 – 9 – 6 – 1

One small example, found by computer search and checked edge by edge. It is not evidence for the conjecture in general.

Dataset cdc-petersen v1 · All cycles of the Petersen graph enumerated; a depth-first search picks five whose edge multiset uses every edge exactly twice; the cover is re-checked edge by edge. Software: python 3.12.15. Exact combinatorics. SHA-256 91dc505f3b7f… · Download JSON

Data
SetEdges
Graph (15 edges)0–1, 1–2, 2–3, 3–4, 4–0, 0–5, 1–6, 2–7, 3–8, 4–9, 5–7, 6–8, 7–9, 8–5, 9–6
Cycle 1: 0 – 1 – 2 – 3 – 4 – 03–4, 2–3, 1–2, 0–1, 0–4
Cycle 2: 0 – 1 – 6 – 8 – 5 – 00–1, 0–5, 6–8, 1–6, 5–8
Cycle 3: 0 – 4 – 9 – 7 – 5 – 07–9, 0–4, 0–5, 4–9, 5–7
Cycle 4: 2 – 3 – 8 – 6 – 9 – 7 – 26–9, 2–3, 7–9, 3–8, 6–8, 2–7
Cycle 5: 1 – 2 – 7 – 5 – 8 – 3 – 4 – 9 – 6 – 13–4, 6–9, 1–2, 1–6, 3–8, 4–9, 5–8, 2–7, 5–7

Visual setup

A triangle covered by two cycle copies

Take the cycle ABC twice in the cover. Every edge then has multiplicity two. The dashed outline indicates a second copy, not extra graph edges.

Reading boundary. This example explains the multiset convention. It is not a construction or proof for all bridgeless multigraphs.

A triangle covered by two cycle copiesA triangle with edges AB, BC and CA is covered by the multiset {ABC, ABC}; each of its three edges is counted twice and total cycle length is six.ABC×2×2×2Cycle ABC, taken twice
Cycle double cover: definitionQuestion scopeTotal cycle length = 2|E|● Proved under stated assumptions

Each edge lies on the cycle twice, so the total length is 2 × 3 = 6.

Text version

A triangle with edges AB, BC and CA is covered by the multiset {ABC, ABC}; each of its three edges is counted twice and total cycle length is six.

Coordinates in the drawing are illustrative unless the caption specifies an exact example.

  1. Cycle double cover: definition

    Proposed

    Every bridgeless graph has a cycle double cover

    Universal existence. The cited 2026 proof and formal endpoint are reported by their sources; independent mathematical assessment is pending.

    Every bridgeless graph has a cycle double cover →

  2. Total cycle length = 2|E|

    Proved

    A double cover has total length twice the edge count

    A counting consequence of a cover, not a proof that every bridgeless graph admits one.

    A double cover has total length twice the edge count →

Sources & review

Authored by OpenMath source curation on 2026-10-13 (AI-assisted curation). Independent review of this visual explanation is pending; linked assertions and relationships have their own assessments.

Results

The question 1

  • Proposed
    Every bridgeless graph has a cycle double cover

    Universal existence. The cited 2026 proof and formal endpoint are reported by their sources; independent mathematical assessment is pending.

    OpenAI 2026Formalized

Background 1

  • Proved
    A double cover has total length twice the edge count

    A counting consequence of a cover, not a proof that every bridgeless graph admits one.

    OpenAI 2026

Connections

Consequences 1

Assuming Every bridgeless graph has a cycle double coverProposed

Approaches

How the problem is attacked, and what each line of attack cannot yet reach.

From nowhere-zero flows to cycle covers

The formal source constructs a flow on a cubic expansion, projects an even cover back to the original graph, and decomposes it into cycles.

Cannot yet reach The exact bridge, loop and multiplicity conventions must match before transferring the conclusion.

Sources & review

Supporting statements

Source-grounded explanation · independent explanation review: pending.

Timeline

  1. A separately authored proof reportProposal

    Shiva Kintali reports a different proof manuscript with Codex assistance.

    A second proposal does not by itself settle either argument’s correctness.

  2. An AI-assisted proof is announcedProposal

    OpenAI reports a full proof and provides a manuscript and formal source.

    First-party completion claims remain under assessment here.

  3. A public full-scope Lean theoremFormalization

    The OpenAI project reports a formalized flow-to-cover construction ending in the universal statement.

    No local OpenMath proof build or independent correspondence review is recorded.

    Also on the Frontier: Cycle double cover conjecture

  4. The classical cycle double cover questionFoundation

    The question asks for edge multiplicity two, not a vertex cover or a partition into disjoint cycles.

    The bridgeless and loopless hypotheses are part of the selected formulation.

Full history with sources →

Evidence

Literature

2 preprints · 1 project

Status OpenMath assessment · Oct 13, 2026.

Formal

1 complete proof

1 formalization below ↓

Reported in sources: A pinned Lean source reports a complete unconditional endpoint for the ordinary conjecture. OpenMath has not built it; source-reported completion does not replace independent mathematical review.

Computation

None recorded

Review

Not yet reviewed

OpenMath assessment: A full proof and an unconditional Lean endpoint are reported in the selected 2026 sources. OpenMath presents them as a proposed resolution pending independent mathematical assessment.

Source comparison and page curation only; independent mathematical review is pending.

OpenMath pilot collection · OpenMath source curation · assessed Oct 13, 2026 · review due Jan 13, 2027

Collection last checked Oct 13, 2026.

Formalizations

Every bridgeless graph has a cycle double cover →

Lean: the full bridgeless multigraph statementComplete formal proof reported externally

Open formal source ↗

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_bridgeless

Commit 577e9d9ea326d520f80672ee69b830bf1d513df5

External proof reports do not establish an OpenMath run, independent statement correspondence, or independent mathematical review.

Sources

Choose a starting point below. Each result links to its exact statement, cited passages and checks.

Start here

Bibliography 3

Research activity · 1 entry

Research direction

Compare the statement and proof evidence

The public theorem and manuscript can be examined alongside Kintali’s separately authored proposal.

Independent mathematical review and a locally reproduced formal build remain pending.

Related statements · context, not additional proved progress

A proof of the cycle double cover conjecture · sources & artifacts →

Cycle double cover in Lean · sources & artifacts →

Three-Bit Flows and Cycle Covers. Part I · sources & artifacts →

Selected literature; source observations and coverage limits are retained in the publication details.

Contributors

OpenAI reports GPT-5.6 Sol Ultra discovery and formal work. Shiva Kintali’s Codex-assisted manuscript is a separate contribution.

Authors & roles

Cycle double cover in Lean →

OpenAI · openai/cdc-lean project

This formal source accompanies the OpenAI AI-assisted proof report; formal checking and human exposition are separate evidence roles.

These are source credits; they do not imply OpenMath accounts, endorsements or independent mathematical review.

Record details
Record version
5
Classification
MSC2020 05C38 / 05C21
Prerequisite level
graduate

Assess the new universal proof, its graph definitions and theorem-to-source correspondence; stronger variants need their own evidence.

Source observations & version history →