State of Proof

2026-07-10-openai-cycle-double-cover · Graph theory

Every finite bridgeless undirected graph has a cycle double cover

Intake record · four gates mapped · no audit gate has run

Current record status

What this docket currently establishes

Intake record · four gates mapped · no audit gate has run. This docket identifies what has been checked and what remains open. It does not validate or reject the manuscript's headline claim beyond the explicitly stated scope.

Claim
Every finite bridgeless undirected graph has a cycle double cover
Source version
Three-page OpenAI manuscript · PDF + Lean 577e9d9
Source SHA-256
b4797f5053d9067329b3dcfcbf913f8bb40d13467453b1300f6d78d08460fc13
Source locked
Last material update
Next open step
Map the manuscript's theorem and graph conventions to the pinned Lean endpoint before drawing any inference from a build

One-minute summary

The three-page manuscript claims the cycle double cover conjecture and ships with a public Lean artifact. Both sources are locked. The first gate is prose-to-Lean statement and definition correspondence; the repository has not been built or mathematically audited in this lab.

Scope of this docket

The planned audit covers prose-to-Lean correspondence, a fresh pinned Lean replay, independent reconstruction and finite stress testing of Lemma 2.2, and the exact hypotheses of the cited graph reductions and flow inputs.

Claim and dependency map

  1. G1 · claim mapped

    Paper-to-Lean statement and definition correspondence

    Depends on: locked PDF · pinned commit

  2. G2 · claim mapped

    Fresh pinned Lean build and kernel replay

    Depends on: G1

  3. G3 · claim mapped

    Independent reconstruction and finite stress tests for Lemma 2.2

    Depends on: G1

  4. G4 · claim mapped

    Cited reductions and nowhere-zero-flow inputs

    Depends on: primary source hypotheses

Evidence routes

formal
Planned: fresh Lean 4.31.0 replay, compiled-source scan, axiom closure, and hashed outputs.
computational
Planned: independent finite property tests for cubic bridgeless multigraphs and admissible flows.
literature
Planned: lock the primary graph-reduction and flow theorems and verify their exact hypotheses.
expert
Planned: graph-theorist review of the cycle-decomposition inference and scope correspondence.

Findings and scope limits

  1. No Lean build, replay, or mathematical audit gate has run in this lab.

  2. A successful formal build would support only the encoded endpoint; it would not by itself establish correspondence with the prose theorem.

Open Steps—where expert eyes are needed

Graph theory and formal verification · audit not started

Do the Lean definitions and endpoint match the manuscript's advertised theorem across loops, parallel edges, connectedness, bridgelessness, and cycle conventions?

Formal replay is meaningful only after the encoded statement is shown to match the public claim.

Source record and provenance

Public manuscript with no asserted arXiv, journal, or referee disposition in the locked source.

Selected and maintained by Material Shift as protocol research. No external sponsor or author involvement is recorded for this case.

Retrieved .

Version and record history

  1. new docket

    2026-07-10-openai-cycle-double-cover

    Manuscript and Lean commit locked; four audit gates mapped; no gate run

Statuses describe evidence collected for a defined scope. They are not peer-review decisions, publication recommendations, or certificates of mathematical truth.