Every finite bridgeless undirected graph has a cycle double cover
Queued record · four gates mapped · no examination route has run
Current record status
What this docket currently establishes
Queued record · four gates mapped · no examination route 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
- Machine-readable record
- JSON record · Atom change feed
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 examined in this lab.
For non-specialists
Why this matters
A nontechnical reading of the claim and its possible consequences. These are implications to consider, not findings of this docket.
In plain English
The manuscript claims that every finite bridgeless undirected graph can have its edges covered exactly twice by a collection of cycles. A Lean formalization is available, but neither its build nor its correspondence to the manuscript has been checked in this docket.
If the claim holds
If the mathematical claim holds, it would establish the stated general graph-theory result. A successful formal check would matter only after confirming that its encoded definitions and theorem match the public claim.
Potential concerns
Small differences in definitions—such as the treatment of loops, parallel edges, connectedness, bridges, and cycles—can change what a formal statement covers. The cited reductions and flow results also need their hypotheses checked.
If it does not hold up
If the proof or its formal correspondence fails, the Lean artifact might still establish a narrower or different statement. It would not by itself settle the advertised theorem.
Scope of this docket
The planned examination 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
Paper-to-Lean statement and definition correspondence
Depends on: locked PDF · pinned commit
Fresh pinned Lean build and kernel replay
Depends on: G1
Independent reconstruction and finite stress tests for Lemma 2.2
Depends on: G1
Cited reductions and nowhere-zero-flow inputs
Depends on: primary source hypotheses
Examination routes
- formal
- Queued · updated 2026-08-26
Planned: fresh Lean 4.31.0 replay, compiled-source scan, axiom closure, and hashed outputs. - computational
- Queued · updated 2026-08-26
Planned: independent finite property tests for cubic bridgeless multigraphs and admissible flows. - literature
- Queued · updated 2026-08-26
Planned: lock the primary graph-reduction and flow theorems and verify their exact hypotheses. - expert
- Queued · updated 2026-08-26
Planned: graph-theorist review of the cycle-decomposition inference and scope correspondence.
Findings and scope limits
No Lean build, replay, or mathematical examination route has run in this lab.
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
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 .
- Preservation
- The manuscript and commit-pinned Lean artifact are separately identified. A public Wayback PDF snapshot was found, but it has not been hash-compared with the locked docket file.
- Record provenance
- Claim map and route plan prepared by Material Shift from the recorded public sources; no mathematical finding or external review is recorded.
- Author contact
- No author outreach, correspondence, response, or author approval is recorded for this docket. Contact the record steward.
Version and record history
-
record provenance
2026-07-10-openai-cycle-double-cover
Record classified as queued; source preservation, route provenance, and author-contact state published
-
new docket
2026-07-10-openai-cycle-double-cover
Manuscript and Lean commit locked; four examination 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.