openmath.dev
Esc

Loading…

↑ ↓ to move↵ to open

Appearance
Appearance

Conjecture · version 2

Every bridgeless graph has a cycle double cover

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.

Explanation

Proof outlines · 2

Evidence

Source reports

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_bridgeless

Commit 577e9d9ea326d520f80672ee69b830bf1d513df5

Connections

In this problem · publication v2 · Selected context

Cycle double cover conjecture →

Primary formulation · Proposed

Relationship not independently reviewed. This concerns its use in this problem.

In this problem · publication v5

Cycle double cover conjecture →

Primary formulation · Proposed

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

Relationship not independently reviewed. This concerns its use in this problem.

Sources

A proof of the cycle double cover conjecture →

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.

Cycle double cover in Lean →

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.

Three-Bit Flows and Cycle Covers. Part I →

Shiva Kintali · Preprint · Publication date Jul 13, 2026

Public manuscript or exposition; publication does not imply independent OpenMath review.

Revision & attribution

Source revision: 2026-07-13. Observed Oct 13, 2026.

Shiva Kintali reports work with Codex; this is a distinct manuscript and has not been adjudicated by OpenMath.

Source updated Jul 13, 2026.

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.

Record details
Claim ID
claim-cycle-double-cover-existence
Statement version
2
SHA-256
627ec968905e9978cfa182b6a1ba0baec3459d00555ce04e8abeeeb6c45fcdc8

Publication records