Reading source record 577e9d9ea326d520f80672ee69b830bf1d513df5. View default cited record →
The source endpoint covers finite loopless bridgeless multigraphs via a formalized eight-flow theorem and a conversion to cycle covers.
Public formal source; build and independent mathematical review are separate checks.
1 cited passage ↓1 problem ↓Record 577e9d9ea326d520f80672ee69b830bf1d513df5 ↓
The exact passages cited in OpenMath. Each passage identifies how its wording was recorded.
The source endpoint covers finite loopless bridgeless multigraphs via a formalized eight-flow theorem and a conversion to cycle covers.
Passage ID: cycle-double-cover:entry:lean:v1
Source item: lean
Source record: cycle-double-cover:source:lean:v1
Explicit citations in versioned problem publications. A citation records a use; it does not confer proof or independent verification.
Problem publication v5
Source assessment
Proposed
Unconditional Lean endpoint reported complete
CDCLean.cycleDoubleCover_of_bridgeless, with no additional project axioms reported.
Observed Oct 13, 2026
Formal declaration
Lean: the full bridgeless multigraph statement
Research activity
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.
History
A public full-scope Lean theorem
Question
Cycle double cover conjecture
Further reading
Inspect the formal statement, assumptions and reported checks.
Linked manuscripts, code and data. External proof reports, statement correspondence and OpenMath execution are separate checks.
Formal code
No OpenMath execution recorded
Public source inspected for statement and assumptions; this proof project has not been executed by OpenMath.
Resource revision: 577e9d9ea326d520f80672ee69b830bf1d513df5
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
CDCLean.cycleDoubleCover_of_bridgelessCommit 577e9d9ea326d520f80672ee69b830bf1d513df5
Recorded authorship
OpenAI · openai/cdc-lean project
OpenAI, openai/cdc-lean project
This formal source accompanies the OpenAI AI-assisted proof report; formal checking and human exposition are separate evidence roles.
OpenMath source records preserve exact citations. Observation dates order these records; they do not establish the latest upstream paper or proof.
Cycle double cover in Lean
OpenMath supplies original paraphrases and links; no proof text is republished.
Source terms ↗