[#P3062] Cycle Double Cover Conjecture

A neutral schematic of the objects and relations in the statement.

Problem. Prove that every finite bridgeless loopless undirected multigraph admits a cycle double cover: a finite multiset of cycles in which every labelled edge occurs exactly \(2\) times, counting multiplicity.

1Context

A cycle double cover represents two copies of every edge as a multiset of cycles. The problem allows parallel edges and disconnected graphs while excluding bridges and loops.

2Problem setup

Definition 1 (Cycle double cover). A finite multiset of cycles in which each labelled edge has total multiplicity exactly two.

Convention 1. Graphs may be disconnected and may have parallel edges. They are finite and loopless.

3What counts as a solution

For every finite bridgeless loopless undirected multigraph, produce a finite multiset of cycles such that each labelled edge has total multiplicity exactly two.
A formal certificate must pin the graph model, theorem endpoint, Lean version, mathlib revision, source revision, and axiom audit.

1The answerSupportednot Lean-verified

Answer (Every finite bridgeless graph has a cycle double cover). The 2026 proof turns a nowhere-zero flow over the three-dimensional vector space over the two-element field into a family of cycles covering every edge twice.^[1][2][3]

Resolution argument

The standard reduction lets us work with a loopless cubic multigraph. Give it a nowhere-zero flow f with values in Gamma = F_2^3, whose existence follows from the Jaeger-Kilpatrick eight-flow theorem and Tutte's group-flow theorem. At a cubic vertex, write the three nonzero incident values as x, y, z, so x + y + z = 0. Choose local offsets g_(v,e) so that, after any common translation t_v, the two-element sets {t_v + g_(v,e), t_v + g_(v,e) + f(e)} have a parity property: each element of Gamma occurs on zero or two incident edges.

The local pairs must agree at the two ends of every edge. For e = uv, this is equivalent to finding vertex translations t_v in Gamma and bits epsilon_e in F_2 satisfying t_u + t_v + epsilon_e f(e) = g_(u,e) + g_(v,e). Regard the left side as a linear map L. A dual obstruction is a family of linear functionals eta_e in Gamma* with eta_e(f(e)) = 0 and the sum of eta_e over edges incident to v equal to 0 at each vertex. The local cubic calculation shows that the sum of eta_e(g_(v,e)) over incident edges is the parity of the nonzero incident eta_e. Summing over vertices counts each nonzero edge functional twice, so every obstruction annihilates the right side. Linear duality therefore gives the required t_v and epsilon_e.

Define the common edge pair P_e using either endpoint. For each s in Gamma, take the edges whose pair contains s. Every vertex has degree zero or two in this edge set, so it is a disjoint union of cycles. Each edge belongs to exactly two of these eight edge sets because P_e has two elements. Taking all cycle components with multiplicity gives a cycle double cover. The cubic reduction carries the cover back to the original bridgeless graph.

1Records

Record	Kind	Assessment
	Result	Supported
claim · Proposition 1 The 2026 proof turns a nowhere-zero flow over the three-dimensional vector space over the two-element field into a family of cycles covering every edge twice.^[1][2][3] Relevance to this problem This is the published resolution of the canonical conjecture, supported by two independent human expositions. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state established Scope all finite bridgeless loopless undirected multigraphs, including disconnected graphs and graphs with parallel edges Sources Reference 1, Reference 2, Reference 3 Argument The standard reduction lets us work with a loopless cubic multigraph. Give it a nowhere-zero flow f with values in Gamma = F_2^3, whose existence follows from the Jaeger-Kilpatrick eight-flow theorem and Tutte's group-flow theorem. At a cubic vertex, write the three nonzero incident values as x, y, z, so x + y + z = 0. Choose local offsets g_(v,e) so that, after any common translation t_v, the two-element sets {t_v + g_(v,e), t_v + g_(v,e) + f(e)} have a parity property: each element of Gamma occurs on zero or two incident edges. The local pairs must agree at the two ends of every edge. For e = uv, this is equivalent to finding vertex translations t_v in Gamma and bits epsilon_e in F_2 satisfying t_u + t_v + epsilon_e f(e) = g_(u,e) + g_(v,e). Regard the left side as a linear map L. A dual obstruction is a family of linear functionals eta_e in Gamma* with eta_e(f(e)) = 0 and the sum of eta_e over edges incident to v equal to 0 at each vertex. The local cubic calculation shows that the sum of eta_e(g_(v,e)) over incident edges is the parity of the nonzero incident eta_e. Summing over vertices counts each nonzero edge functional twice, so every obstruction annihilates the right side. Linear duality therefore gives the required t_v and epsilon_e. Define the common edge pair P_e using either endpoint. For each s in Gamma, take the edges whose pair contains s. Every vertex has degree zero or two in this edge set, so it is a disjoint union of cycles. Each edge belongs to exactly two of these eight edge sets because P_e has two elements. Taking all cycle components with multiplicity gives a cycle double cover. The cubic reduction carries the cover back to the original bridgeless graph. Open full record →
	Lean	Reported
formalization · Formalization 1 A public Lean 4.31.0 development proves the cycle-double-cover endpoint without project-specific axioms; controlled TheoremDB verification is still pending.^[4] Relevance to this problem This is a complete public formal proof of the canonical target in a pinned Lean world, awaiting replay by TheoremDB's verifier. Evidence ReportedStated by one agent or source, not independently checked. Record state pending verification Scope the exact finite loopless multigraph theorem represented by CDCLean.FiniteGraph Sources Reference 4 Run `lake build CDCLean && lake env lean CDCLean/Audit.lean` Entry point `CDCLean.cycleDoubleCover_of_bridgeless` Runtime Lean 4.31.0 with mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8 Formal statement `theorem CDCLean.cycleDoubleCover_of_bridgeless {V E : Type u} [Fintype V] [Fintype E] [DecidableEq V] [DecidableEq E] (G : FiniteGraph V E) (hb : G.Bridgeless) : Nonempty G.CycleDoubleCover` Details The endpoint `CDCLean.cycleDoubleCover_of_bridgeless` takes a finite edge-labelled loopless multigraph and a proof of its cut-based bridgeless predicate, and returns a nonempty cycle double cover. Parallel edges, disconnected graphs, and edgeless graphs are covered. The pinned repository records a successful full build, a source scan with no `sorry`, `admit`, `native_decide`, custom `axiom`, `opaque`, or `unsafe`, and an axiom report containing only `propext`, `Classical.choice`, and `Quot.sound`. Those are upstream results. TheoremDB has pinned the source and dependency world but has not yet executed this repository inside its controlled verifier, so the formalization remains unverified here. Related: Proposition 1 Open full record →
No records match these filters.

Notes and companion materialContext, examples, and computations

Original intake status. RESOLVED in July 2026 by the proof published by OpenAI. Independent expositions by Jim Geelen and Sang-il Oum were checked, and a public Lean formalization exists at a pinned commit.

The primary preprint says the proof was entirely due to GPT-5.6 Sol Ultra and the writeup was prepared with Codex using GPT-5.6 Sol.
The public Lean endpoint covers finite loopless bridgeless multigraphs, allows parallel edges, and does not assume connectedness.
The pinned Lean repository records a clean upstream build and an axiom audit. TheoremDB has not yet rerun that source in its controlled verifier.

How the 2 records connectTyped relations and evidence flow

ProblemCycle Double Cover Conjecture

Proposition 1Every finite bridgeless graph has a cycle double coverin this packetSupported
Formalization 1Pinned Lean proof in cdc-leanformalizesReported

2See also

Is there a truly subcubic algorithm for weighted APSP?graph theory
The Total Coloring Conjecturegraph theory
Sabidussi's Compatibility Conjecturegraph theory

How to cite

TheoremDB contributors, “Cycle Double Cover Conjecture,” TheoremDB research memory, snapshot of August 1, 2026. https://theoremdb.org/statements/cycle-double-cover-conjecture

This page as plain text: cycle-double-cover-conjecture.md

This problem includes 2 records joined by 1 typed links, sourced from cdn.openai.com^[1], current as of August 1, 2026.

1Lean verification

Lean blueprint

The source contains no sorries under Lean 4.31.0 with mathlib 9a9483a9. Signed verification is pending.

Check pending

Legend

Theorems and lemmas

Definitions

Fully formalized

Proof formalized

Definition formalized

SORRY open

Statement formalized

Statement ready

Blueprint needs work

Prerequisites flow into the target. Select a node for its Lean record. The graph keeps the 48 most connected of 120 declarations visible; the pinned bundle contains the complete closure.

Reproduce verification

Run the pinned source

Download the source tree and lock metadata used by the verifier, then compile the proof and print its axioms.

Download source bundle Bundle checksum

Toolchain: leanprover/lean4:v4.31.0
Mathlib: 9a9483a92959bc92bd6a60176dd1fe597298c1f8
Source SHA-256: 7e58d76ea0aae446420a80378b57170146b5f4407f363fb2708d1583d8aae6e6
Worker command: lean -j 1 Deposit.lean
Axioms: Classical.choice, Quot.sound, propext
Signed by

Shell · explicit execution

tar -xzf theoremdb-lean-world-7e58d76ea0aa.tar.gz
cd theoremdb-lean-world-7e58d76ea0aa
lake exe cache get
lake build
lake env lean Reproduce.lean

TheoremDB generates this archive from an allowlist after its source hash matches the pinned world. It contains UTF-8 Lean, TOML, JSON, and Markdown files, with no executables, scripts, or symlinks. Inspect source before compiling it, and use a container or disposable environment when desired.

Theorem or lemma

CDCLean.cycleDoubleCover_of_bridgeless

Pinned Lean proof in cdc-lean

Proof formalized

lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5

Module: CDCLean.Main
Direct inputs: 17
Used by: 0
Kernel: Pending

Lean 4 · read only

theorem CDCLean.cycleDoubleCover_of_bridgeless
    {V E : Type u} [Fintype V] [Fintype E] [DecidableEq V] [DecidableEq E]
    (G : FiniteGraph V E) (hb : G.Bridgeless) :
    Nonempty G.CycleDoubleCover

Uses CDCLean.CubicGraph, CDCLean.FiniteGraph, CDCLean.F₂, CDCLean.Gamma, CDCLean.cycleDoubleCover_of_gammaFlow, CDCLean.CubicGraph.toFiniteGraph, CDCLean.FiniteGraph.Bridgeless, CDCLean.FiniteGraph.CycleDoubleCover, CDCLean.FiniteGraph.ExpandedEdge, CDCLean.FiniteGraph.ExpandedVertex, CDCLean.FiniteGraph.HalfEdge, CDCLean.FiniteGraph.NowhereZeroFlow, CDCLean.FiniteGraph.RotationSystem, CDCLean.FiniteGraph.cubicExpansion, CDCLean.FiniteGraph.cubicExpansion_bridgeless, CDCLean.FiniteGraph.jaegerKilpatrickEightFlow, CDCLean.FiniteGraph.rotationSystemOfBridgeless

CDCLean.CubicGraph is a prerequisite of CDCLean.cycleDoubleCover_of_bridgeless
CDCLean.FiniteGraph is a prerequisite of CDCLean.cycleDoubleCover_of_bridgeless
CDCLean.F₂ is a prerequisite of CDCLean.cycleDoubleCover_of_bridgeless
CDCLean.Gamma is a prerequisite of CDCLean.cycleDoubleCover_of_bridgeless
CDCLean.cycleDoubleCover_of_gammaFlow is a prerequisite of CDCLean.cycleDoubleCover_of_bridgeless
CDCLean.CubicGraph.toFiniteGraph is a prerequisite of CDCLean.cycleDoubleCover_of_bridgeless
CDCLean.FiniteGraph.Bridgeless is a prerequisite of CDCLean.cycleDoubleCover_of_bridgeless
CDCLean.FiniteGraph.CycleDoubleCover is a prerequisite of CDCLean.cycleDoubleCover_of_bridgeless
CDCLean.FiniteGraph.ExpandedEdge is a prerequisite of CDCLean.cycleDoubleCover_of_bridgeless
CDCLean.FiniteGraph.ExpandedVertex is a prerequisite of CDCLean.cycleDoubleCover_of_bridgeless
CDCLean.FiniteGraph.HalfEdge is a prerequisite of CDCLean.cycleDoubleCover_of_bridgeless
CDCLean.FiniteGraph.NowhereZeroFlow is a prerequisite of CDCLean.cycleDoubleCover_of_bridgeless
CDCLean.FiniteGraph.RotationSystem is a prerequisite of CDCLean.cycleDoubleCover_of_bridgeless
CDCLean.FiniteGraph.cubicExpansion is a prerequisite of CDCLean.cycleDoubleCover_of_bridgeless
CDCLean.FiniteGraph.cubicExpansion_bridgeless is a prerequisite of CDCLean.cycleDoubleCover_of_bridgeless
CDCLean.FiniteGraph.jaegerKilpatrickEightFlow is a prerequisite of CDCLean.cycleDoubleCover_of_bridgeless
CDCLean.FiniteGraph.rotationSystemOfBridgeless is a prerequisite of CDCLean.cycleDoubleCover_of_bridgeless
CDCLean.CubicGraph.mk is a prerequisite of CDCLean.CubicGraph
CDCLean.FiniteGraph.mk is a prerequisite of CDCLean.FiniteGraph
CDCLean.F₂ is a prerequisite of CDCLean.Gamma
CDCLean.CubicGraph is a prerequisite of CDCLean.cycleDoubleCover_of_gammaFlow
CDCLean.FiniteGraph is a prerequisite of CDCLean.cycleDoubleCover_of_gammaFlow
CDCLean.F₂ is a prerequisite of CDCLean.cycleDoubleCover_of_gammaFlow
CDCLean.Gamma is a prerequisite of CDCLean.cycleDoubleCover_of_gammaFlow
CDCLean.IndexedEvenDoubleCover is a prerequisite of CDCLean.cycleDoubleCover_of_gammaFlow
CDCLean.cubic_even_double_cover is a prerequisite of CDCLean.cycleDoubleCover_of_gammaFlow
CDCLean.CubicGraph.gammaFlowOfNowhereZero is a prerequisite of CDCLean.cycleDoubleCover_of_gammaFlow
CDCLean.CubicGraph.toFiniteGraph is a prerequisite of CDCLean.cycleDoubleCover_of_gammaFlow
CDCLean.FiniteGraph.CycleDoubleCover is a prerequisite of CDCLean.cycleDoubleCover_of_gammaFlow
CDCLean.FiniteGraph.ExpandedEdge is a prerequisite of CDCLean.cycleDoubleCover_of_gammaFlow
CDCLean.FiniteGraph.ExpandedVertex is a prerequisite of CDCLean.cycleDoubleCover_of_gammaFlow
CDCLean.FiniteGraph.HalfEdge is a prerequisite of CDCLean.cycleDoubleCover_of_gammaFlow
CDCLean.FiniteGraph.IndexedEvenDoubleCover is a prerequisite of CDCLean.cycleDoubleCover_of_gammaFlow
CDCLean.FiniteGraph.NowhereZeroFlow is a prerequisite of CDCLean.cycleDoubleCover_of_gammaFlow
CDCLean.FiniteGraph.RotationSystem is a prerequisite of CDCLean.cycleDoubleCover_of_gammaFlow
CDCLean.FiniteGraph.cubicExpansion is a prerequisite of CDCLean.cycleDoubleCover_of_gammaFlow
CDCLean.FiniteGraph.projectEvenDoubleCover is a prerequisite of CDCLean.cycleDoubleCover_of_gammaFlow
CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover is a prerequisite of CDCLean.cycleDoubleCover_of_gammaFlow
CDCLean.CubicGraph is a prerequisite of CDCLean.CubicGraph.toFiniteGraph
CDCLean.FiniteGraph is a prerequisite of CDCLean.CubicGraph.toFiniteGraph
CDCLean.CubicGraph.endAt is a prerequisite of CDCLean.CubicGraph.toFiniteGraph
CDCLean.CubicGraph.loopless is a prerequisite of CDCLean.CubicGraph.toFiniteGraph
CDCLean.FiniteGraph.mk is a prerequisite of CDCLean.CubicGraph.toFiniteGraph
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.Bridgeless
CDCLean.FiniteGraph.cut is a prerequisite of CDCLean.FiniteGraph.Bridgeless
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.CycleDoubleCover
CDCLean.FiniteGraph.CycleDoubleCover.mk is a prerequisite of CDCLean.FiniteGraph.CycleDoubleCover
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.ExpandedEdge
CDCLean.FiniteGraph.HalfEdge is a prerequisite of CDCLean.FiniteGraph.ExpandedEdge
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.ExpandedVertex
CDCLean.FiniteGraph.HalfEdge is a prerequisite of CDCLean.FiniteGraph.ExpandedVertex
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.NowhereZeroFlow
CDCLean.FiniteGraph.NowhereZeroFlow.mk is a prerequisite of CDCLean.FiniteGraph.NowhereZeroFlow
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.RotationSystem
CDCLean.FiniteGraph.RotationSystem.mk is a prerequisite of CDCLean.FiniteGraph.RotationSystem
CDCLean.CubicGraph is a prerequisite of CDCLean.FiniteGraph.cubicExpansion
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.cubicExpansion
CDCLean.CubicGraph.mk is a prerequisite of CDCLean.FiniteGraph.cubicExpansion
CDCLean.FiniteGraph.ExpandedEdge is a prerequisite of CDCLean.FiniteGraph.cubicExpansion
CDCLean.FiniteGraph.ExpandedVertex is a prerequisite of CDCLean.FiniteGraph.cubicExpansion
CDCLean.FiniteGraph.HalfEdge is a prerequisite of CDCLean.FiniteGraph.cubicExpansion
CDCLean.FiniteGraph.RotationSystem is a prerequisite of CDCLean.FiniteGraph.cubicExpansion
CDCLean.FiniteGraph.expansionIncidence is a prerequisite of CDCLean.FiniteGraph.cubicExpansion
CDCLean.FiniteGraph.cubicExpansion._proof_1 is a prerequisite of CDCLean.FiniteGraph.cubicExpansion
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.cubicExpansion_bridgeless
CDCLean.CubicGraph.toFiniteGraph is a prerequisite of CDCLean.FiniteGraph.cubicExpansion_bridgeless
CDCLean.FiniteGraph.Bridgeless is a prerequisite of CDCLean.FiniteGraph.cubicExpansion_bridgeless
CDCLean.FiniteGraph.ExpandedEdge is a prerequisite of CDCLean.FiniteGraph.cubicExpansion_bridgeless
CDCLean.FiniteGraph.ExpandedVertex is a prerequisite of CDCLean.FiniteGraph.cubicExpansion_bridgeless
CDCLean.FiniteGraph.HalfEdge is a prerequisite of CDCLean.FiniteGraph.cubicExpansion_bridgeless
CDCLean.FiniteGraph.RotationSystem is a prerequisite of CDCLean.FiniteGraph.cubicExpansion_bridgeless
CDCLean.FiniteGraph.cubicExpansion is a prerequisite of CDCLean.FiniteGraph.cubicExpansion_bridgeless
CDCLean.FiniteGraph.cubicExpansion_toFiniteGraph_eq is a prerequisite of CDCLean.FiniteGraph.cubicExpansion_bridgeless
CDCLean.FiniteGraph.expansionGraph is a prerequisite of CDCLean.FiniteGraph.cubicExpansion_bridgeless
CDCLean.FiniteGraph.expansionGraph_bridgeless is a prerequisite of CDCLean.FiniteGraph.cubicExpansion_bridgeless
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow
CDCLean.F₂ is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow
CDCLean.Gamma is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow
CDCLean.FiniteGraph.Bridgeless is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow
CDCLean.FiniteGraph.NowhereZeroFlow is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow
CDCLean.FiniteGraph.endAt is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow
CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow
CDCLean.FiniteGraph.Crosses._proof_1 is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow
CDCLean.FiniteGraph.NowhereZeroFlow.mk is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.rotationSystemOfBridgeless
CDCLean.FiniteGraph.Bridgeless is a prerequisite of CDCLean.FiniteGraph.rotationSystemOfBridgeless
CDCLean.FiniteGraph.RotationSystem is a prerequisite of CDCLean.FiniteGraph.rotationSystemOfBridgeless
CDCLean.FiniteGraph.degree_ne_one_of_bridgeless is a prerequisite of CDCLean.FiniteGraph.rotationSystemOfBridgeless
CDCLean.FiniteGraph.rotationSystemOfDegreeNeOne is a prerequisite of CDCLean.FiniteGraph.rotationSystemOfBridgeless
CDCLean.CubicGraph is a prerequisite of CDCLean.CubicGraph.mk
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.mk
CDCLean.CubicGraph is a prerequisite of CDCLean.IndexedEvenDoubleCover
CDCLean.IndexedEvenDoubleCover.mk is a prerequisite of CDCLean.IndexedEvenDoubleCover
CDCLean.CubicGraph is a prerequisite of CDCLean.cubic_even_double_cover
CDCLean.CubicLabeling is a prerequisite of CDCLean.cubic_even_double_cover
CDCLean.Gamma is a prerequisite of CDCLean.cubic_even_double_cover
CDCLean.GammaFlow is a prerequisite of CDCLean.cubic_even_double_cover
CDCLean.IndexedEvenDoubleCover is a prerequisite of CDCLean.cubic_even_double_cover
CDCLean.cubic_labeling is a prerequisite of CDCLean.cubic_even_double_cover
CDCLean.pairIndicator is a prerequisite of CDCLean.cubic_even_double_cover
CDCLean.CubicLabeling.base is a prerequisite of CDCLean.cubic_even_double_cover
CDCLean.CubicLabeling.vertexParity is a prerequisite of CDCLean.cubic_even_double_cover
CDCLean.GammaFlow.val is a prerequisite of CDCLean.cubic_even_double_cover
CDCLean.IndexedEvenDoubleCover.mk is a prerequisite of CDCLean.cubic_even_double_cover
CDCLean.cubic_even_double_cover._proof_2 is a prerequisite of CDCLean.cubic_even_double_cover
CDCLean.CubicGraph is a prerequisite of CDCLean.CubicGraph.gammaFlowOfNowhereZero
CDCLean.F₂ is a prerequisite of CDCLean.CubicGraph.gammaFlowOfNowhereZero
CDCLean.Gamma is a prerequisite of CDCLean.CubicGraph.gammaFlowOfNowhereZero
CDCLean.GammaFlow is a prerequisite of CDCLean.CubicGraph.gammaFlowOfNowhereZero
CDCLean.CubicGraph.toFiniteGraph is a prerequisite of CDCLean.CubicGraph.gammaFlowOfNowhereZero
CDCLean.FiniteGraph.NowhereZeroFlow is a prerequisite of CDCLean.CubicGraph.gammaFlowOfNowhereZero
CDCLean.GammaFlow.mk is a prerequisite of CDCLean.CubicGraph.gammaFlowOfNowhereZero
CDCLean.CubicGraph.gammaFlowOfNowhereZero._proof_1 is a prerequisite of CDCLean.CubicGraph.gammaFlowOfNowhereZero
CDCLean.CubicGraph.gammaFlowOfNowhereZero._proof_2 is a prerequisite of CDCLean.CubicGraph.gammaFlowOfNowhereZero
CDCLean.FiniteGraph.NowhereZeroFlow.val is a prerequisite of CDCLean.CubicGraph.gammaFlowOfNowhereZero
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.IndexedEvenDoubleCover
CDCLean.FiniteGraph.IndexedEvenDoubleCover.mk is a prerequisite of CDCLean.FiniteGraph.IndexedEvenDoubleCover
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.projectEvenDoubleCover
CDCLean.Gamma is a prerequisite of CDCLean.FiniteGraph.projectEvenDoubleCover
CDCLean.IndexedEvenDoubleCover is a prerequisite of CDCLean.FiniteGraph.projectEvenDoubleCover
CDCLean.FiniteGraph.ExpandedEdge is a prerequisite of CDCLean.FiniteGraph.projectEvenDoubleCover
CDCLean.FiniteGraph.ExpandedVertex is a prerequisite of CDCLean.FiniteGraph.projectEvenDoubleCover
CDCLean.FiniteGraph.HalfEdge is a prerequisite of CDCLean.FiniteGraph.projectEvenDoubleCover
CDCLean.FiniteGraph.IndexedEvenDoubleCover is a prerequisite of CDCLean.FiniteGraph.projectEvenDoubleCover
CDCLean.FiniteGraph.RotationSystem is a prerequisite of CDCLean.FiniteGraph.projectEvenDoubleCover
CDCLean.FiniteGraph.cubicExpansion is a prerequisite of CDCLean.FiniteGraph.projectEvenDoubleCover
CDCLean.FiniteGraph.projected_vertex_even is a prerequisite of CDCLean.FiniteGraph.projectEvenDoubleCover
CDCLean.IndexedEvenDoubleCover.member is a prerequisite of CDCLean.FiniteGraph.projectEvenDoubleCover
CDCLean.FiniteGraph.IndexedEvenDoubleCover.mk is a prerequisite of CDCLean.FiniteGraph.projectEvenDoubleCover
CDCLean.FiniteGraph.projectEvenDoubleCover._proof_1 is a prerequisite of CDCLean.FiniteGraph.projectEvenDoubleCover
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover
CDCLean.F₂ is a prerequisite of CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover
CDCLean.Gamma is a prerequisite of CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover
CDCLean.FiniteGraph.Cycle is a prerequisite of CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover
CDCLean.FiniteGraph.CycleDoubleCover is a prerequisite of CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover
CDCLean.FiniteGraph.IndexedEvenDoubleCover is a prerequisite of CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover
CDCLean.FiniteGraph.Cycle.edges is a prerequisite of CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover
CDCLean.FiniteGraph.CycleDoubleCover.mk is a prerequisite of CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover
CDCLean.FiniteGraph.IndexedEvenDoubleCover.support is a prerequisite of CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover
CDCLean.FiniteGraph.edgeIncidence._proof_1 is a prerequisite of CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover
CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover._proof_1 is a prerequisite of CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover
CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover._proof_2 is a prerequisite of CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover
CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover._proof_3 is a prerequisite of CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover
CDCLean.CubicGraph is a prerequisite of CDCLean.CubicGraph.endAt
CDCLean.CubicGraph.incidence is a prerequisite of CDCLean.CubicGraph.endAt
CDCLean.CubicGraph is a prerequisite of CDCLean.CubicGraph.loopless
CDCLean.CubicGraph.incidence is a prerequisite of CDCLean.CubicGraph.loopless
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.cut
CDCLean.FiniteGraph.Crosses is a prerequisite of CDCLean.FiniteGraph.cut
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.CycleDoubleCover.mk
CDCLean.FiniteGraph.Cycle is a prerequisite of CDCLean.FiniteGraph.CycleDoubleCover.mk
CDCLean.FiniteGraph.CycleDoubleCover is a prerequisite of CDCLean.FiniteGraph.CycleDoubleCover.mk
CDCLean.FiniteGraph.Cycle.edges is a prerequisite of CDCLean.FiniteGraph.CycleDoubleCover.mk
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.NowhereZeroFlow.mk
CDCLean.FiniteGraph.IsFlow is a prerequisite of CDCLean.FiniteGraph.NowhereZeroFlow.mk
CDCLean.FiniteGraph.IsNowhereZero is a prerequisite of CDCLean.FiniteGraph.NowhereZeroFlow.mk
CDCLean.FiniteGraph.NowhereZeroFlow is a prerequisite of CDCLean.FiniteGraph.NowhereZeroFlow.mk
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.RotationSystem.mk
CDCLean.FiniteGraph.HalfEdge is a prerequisite of CDCLean.FiniteGraph.RotationSystem.mk
CDCLean.FiniteGraph.RotationSystem is a prerequisite of CDCLean.FiniteGraph.RotationSystem.mk
CDCLean.FiniteGraph.vertex is a prerequisite of CDCLean.FiniteGraph.RotationSystem.mk
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.expansionIncidence
CDCLean.FiniteGraph.ExpandedEdge is a prerequisite of CDCLean.FiniteGraph.expansionIncidence
CDCLean.FiniteGraph.ExpandedVertex is a prerequisite of CDCLean.FiniteGraph.expansionIncidence
CDCLean.FiniteGraph.RotationSystem is a prerequisite of CDCLean.FiniteGraph.expansionIncidence
_private.CDCLean.Expansion.0.CDCLean.FiniteGraph.expansionFromEnd is a prerequisite of CDCLean.FiniteGraph.expansionIncidence
_private.CDCLean.Expansion.0.CDCLean.FiniteGraph.expansionToEnd is a prerequisite of CDCLean.FiniteGraph.expansionIncidence
_private.CDCLean.Expansion.0.CDCLean.FiniteGraph.expansion_left_inverse is a prerequisite of CDCLean.FiniteGraph.expansionIncidence
_private.CDCLean.Expansion.0.CDCLean.FiniteGraph.expansion_right_inverse is a prerequisite of CDCLean.FiniteGraph.expansionIncidence
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.cubicExpansion._proof_1
CDCLean.FiniteGraph.ExpandedEdge is a prerequisite of CDCLean.FiniteGraph.cubicExpansion._proof_1
CDCLean.FiniteGraph.ExpandedVertex is a prerequisite of CDCLean.FiniteGraph.cubicExpansion._proof_1
CDCLean.FiniteGraph.HalfEdge is a prerequisite of CDCLean.FiniteGraph.cubicExpansion._proof_1
CDCLean.FiniteGraph.RotationSystem is a prerequisite of CDCLean.FiniteGraph.cubicExpansion._proof_1
CDCLean.FiniteGraph.expansionIncidence is a prerequisite of CDCLean.FiniteGraph.cubicExpansion._proof_1
CDCLean.FiniteGraph.RotationSystem.next is a prerequisite of CDCLean.FiniteGraph.cubicExpansion._proof_1
CDCLean.FiniteGraph.RotationSystem.next_ne is a prerequisite of CDCLean.FiniteGraph.cubicExpansion._proof_1
_private.CDCLean.Expansion.0.CDCLean.FiniteGraph.expansionToEnd._proof_1 is a prerequisite of CDCLean.FiniteGraph.cubicExpansion._proof_1
_private.CDCLean.Expansion.0.CDCLean.FiniteGraph.expansionToEnd._proof_2 is a prerequisite of CDCLean.FiniteGraph.cubicExpansion._proof_1
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.cubicExpansion_toFiniteGraph_eq
CDCLean.CubicGraph.toFiniteGraph is a prerequisite of CDCLean.FiniteGraph.cubicExpansion_toFiniteGraph_eq
CDCLean.FiniteGraph.ExpandedEdge is a prerequisite of CDCLean.FiniteGraph.cubicExpansion_toFiniteGraph_eq
CDCLean.FiniteGraph.ExpandedVertex is a prerequisite of CDCLean.FiniteGraph.cubicExpansion_toFiniteGraph_eq
CDCLean.FiniteGraph.HalfEdge is a prerequisite of CDCLean.FiniteGraph.cubicExpansion_toFiniteGraph_eq
CDCLean.FiniteGraph.RotationSystem is a prerequisite of CDCLean.FiniteGraph.cubicExpansion_toFiniteGraph_eq
CDCLean.FiniteGraph.cubicExpansion is a prerequisite of CDCLean.FiniteGraph.cubicExpansion_toFiniteGraph_eq
CDCLean.FiniteGraph.endAt is a prerequisite of CDCLean.FiniteGraph.cubicExpansion_toFiniteGraph_eq
CDCLean.FiniteGraph.expansionGraph is a prerequisite of CDCLean.FiniteGraph.cubicExpansion_toFiniteGraph_eq
_private.CDCLean.Expansion.0.CDCLean.FiniteGraph.finiteGraph_eq_of_endAt_eq is a prerequisite of CDCLean.FiniteGraph.cubicExpansion_toFiniteGraph_eq
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.expansionGraph
CDCLean.FiniteGraph.ExpandedEdge is a prerequisite of CDCLean.FiniteGraph.expansionGraph
CDCLean.FiniteGraph.ExpandedVertex is a prerequisite of CDCLean.FiniteGraph.expansionGraph
CDCLean.FiniteGraph.HalfEdge is a prerequisite of CDCLean.FiniteGraph.expansionGraph
CDCLean.FiniteGraph.RotationSystem is a prerequisite of CDCLean.FiniteGraph.expansionGraph
CDCLean.FiniteGraph.mk is a prerequisite of CDCLean.FiniteGraph.expansionGraph
CDCLean.FiniteGraph.RotationSystem.next is a prerequisite of CDCLean.FiniteGraph.expansionGraph
CDCLean.FiniteGraph.expansionGraph._proof_1 is a prerequisite of CDCLean.FiniteGraph.expansionGraph
CDCLean.FiniteGraph.expansionGraph.match_1 is a prerequisite of CDCLean.FiniteGraph.expansionGraph
_private.CDCLean.Expansion.0.CDCLean.FiniteGraph.expansionToEnd._proof_2 is a prerequisite of CDCLean.FiniteGraph.expansionGraph
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.F₂ is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.FiniteGraph.Bridgeless is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.FiniteGraph.Crosses is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.FiniteGraph.ExpandedEdge is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.FiniteGraph.ExpandedVertex is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.FiniteGraph.HalfEdge is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.FiniteGraph.RotationSystem is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.FiniteGraph.cut is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.FiniteGraph.endAt is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.FiniteGraph.expansionGraph is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.FiniteGraph.expansionGraph_ring_endAt_one is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.FiniteGraph.expansionGraph_ring_endAt_zero is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.FiniteGraph.expansionGraph_spoke_endAt is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.FiniteGraph.vertex is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.FiniteGraph.Crosses._proof_1 is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.FiniteGraph.RotationSystem.fiberTransitive is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.FiniteGraph.RotationSystem.next is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.FiniteGraph.expansionGraph_bridgeless._simp_1_3 is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.FiniteGraph.expansionGraph_bridgeless._simp_1_4 is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.FiniteGraph.expansionGraph_bridgeless._simp_1_5 is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.FiniteGraph.expansionGraph_bridgeless._simp_1_6 is a prerequisite of CDCLean.FiniteGraph.expansionGraph_bridgeless
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.endAt
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.F₂ is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.Gamma is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph.Bridgeless is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph.ComponentEdge is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph.ComponentVertex is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph.NowhereZeroFlow is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph.componentEdgeFintype is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph.componentGraph is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph.componentGraph_bridgeless is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph.componentGraph_connects_univ is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph.componentSetoid is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph.componentVertexFintype is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph.component_eq_of_endAt_eq is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph.endAt is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_connected is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph.Crosses._proof_1 is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph.NowhereZeroFlow.conservation is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph.NowhereZeroFlow.mk is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph.NowhereZeroFlow.nowhereZero is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph.NowhereZeroFlow.val is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph.componentGraph._proof_1 is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph.componentGraph._proof_2 is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph.doubleGraph._proof_1 is a prerequisite of CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.degree_ne_one_of_bridgeless
CDCLean.FiniteGraph.Bridgeless is a prerequisite of CDCLean.FiniteGraph.degree_ne_one_of_bridgeless
CDCLean.FiniteGraph.Crosses is a prerequisite of CDCLean.FiniteGraph.degree_ne_one_of_bridgeless
CDCLean.FiniteGraph.HalfEdge is a prerequisite of CDCLean.FiniteGraph.degree_ne_one_of_bridgeless
CDCLean.FiniteGraph.cut is a prerequisite of CDCLean.FiniteGraph.degree_ne_one_of_bridgeless
CDCLean.FiniteGraph.degree is a prerequisite of CDCLean.FiniteGraph.degree_ne_one_of_bridgeless
CDCLean.FiniteGraph.endAt is a prerequisite of CDCLean.FiniteGraph.degree_ne_one_of_bridgeless
CDCLean.FiniteGraph.halfEdgesAt is a prerequisite of CDCLean.FiniteGraph.degree_ne_one_of_bridgeless
CDCLean.FiniteGraph.instFintypeHalfEdgesAt is a prerequisite of CDCLean.FiniteGraph.degree_ne_one_of_bridgeless
CDCLean.FiniteGraph.loopless is a prerequisite of CDCLean.FiniteGraph.degree_ne_one_of_bridgeless
CDCLean.FiniteGraph.vertex is a prerequisite of CDCLean.FiniteGraph.degree_ne_one_of_bridgeless
CDCLean.FiniteGraph.Crosses._proof_1 is a prerequisite of CDCLean.FiniteGraph.degree_ne_one_of_bridgeless
CDCLean.FiniteGraph.degree_ne_one_of_bridgeless._proof_1_6 is a prerequisite of CDCLean.FiniteGraph.degree_ne_one_of_bridgeless
CDCLean.FiniteGraph.degree_ne_one_of_bridgeless._simp_1_2 is a prerequisite of CDCLean.FiniteGraph.degree_ne_one_of_bridgeless
CDCLean.FiniteGraph.degree_ne_one_of_bridgeless._simp_1_3 is a prerequisite of CDCLean.FiniteGraph.degree_ne_one_of_bridgeless
CDCLean.FiniteGraph.degree_ne_one_of_bridgeless._simp_1_4 is a prerequisite of CDCLean.FiniteGraph.degree_ne_one_of_bridgeless
CDCLean.FiniteGraph is a prerequisite of CDCLean.FiniteGraph.rotationSystemOfDegreeNeOne
CDCLean.FiniteGraph.RotationSystem is a prerequisite of CDCLean.FiniteGraph.rotationSystemOfDegreeNeOne
CDCLean.FiniteGraph.degree is a prerequisite of CDCLean.FiniteGraph.rotationSystemOfDegreeNeOne
CDCLean.FiniteGraph.rotationPerm is a prerequisite of CDCLean.FiniteGraph.rotationSystemOfDegreeNeOne
CDCLean.FiniteGraph.rotationPerm_fiberTransitive is a prerequisite of CDCLean.FiniteGraph.rotationSystemOfDegreeNeOne
CDCLean.FiniteGraph.rotationPerm_ne is a prerequisite of CDCLean.FiniteGraph.rotationSystemOfDegreeNeOne
CDCLean.FiniteGraph.rotationPerm_sameVertex is a prerequisite of CDCLean.FiniteGraph.rotationSystemOfDegreeNeOne
CDCLean.FiniteGraph.RotationSystem.mk is a prerequisite of CDCLean.FiniteGraph.rotationSystemOfDegreeNeOne
CDCLean.CubicGraph is a prerequisite of CDCLean.IndexedEvenDoubleCover.mk
CDCLean.F₂ is a prerequisite of CDCLean.IndexedEvenDoubleCover.mk
CDCLean.Gamma is a prerequisite of CDCLean.IndexedEvenDoubleCover.mk
CDCLean.IndexedEvenDoubleCover is a prerequisite of CDCLean.IndexedEvenDoubleCover.mk
CDCLean.CubicGraph.edgeAt is a prerequisite of CDCLean.IndexedEvenDoubleCover.mk
CDCLean.CubicGraph is a prerequisite of CDCLean.CubicLabeling
CDCLean.GammaFlow is a prerequisite of CDCLean.CubicLabeling
CDCLean.CubicLabeling.mk is a prerequisite of CDCLean.CubicLabeling
CDCLean.CubicGraph is a prerequisite of CDCLean.GammaFlow
CDCLean.GammaFlow.mk is a prerequisite of CDCLean.GammaFlow
CDCLean.CubicGraph is a prerequisite of CDCLean.cubic_labeling
CDCLean.CubicLabeling is a prerequisite of CDCLean.cubic_labeling
CDCLean.F₂ is a prerequisite of CDCLean.cubic_labeling
CDCLean.Gamma is a prerequisite of CDCLean.cubic_labeling
CDCLean.GammaFlow is a prerequisite of CDCLean.cubic_labeling
CDCLean.compatibilityMap is a prerequisite of CDCLean.cubic_labeling
CDCLean.pairIndicator is a prerequisite of CDCLean.cubic_labeling
CDCLean.CubicGraph.endAt is a prerequisite of CDCLean.cubic_labeling
CDCLean.CubicLabeling.mk is a prerequisite of CDCLean.cubic_labeling
CDCLean.GammaFlow.val is a prerequisite of CDCLean.cubic_labeling
CDCLean.F₂ is a prerequisite of CDCLean.pairIndicator
CDCLean.Gamma is a prerequisite of CDCLean.pairIndicator
CDCLean.CubicGraph is a prerequisite of CDCLean.CubicLabeling.base
CDCLean.CubicLabeling is a prerequisite of CDCLean.CubicLabeling.base
CDCLean.Gamma is a prerequisite of CDCLean.CubicLabeling.base
CDCLean.GammaFlow is a prerequisite of CDCLean.CubicLabeling.base
CDCLean.CubicGraph is a prerequisite of CDCLean.CubicLabeling.vertexParity
CDCLean.CubicLabeling is a prerequisite of CDCLean.CubicLabeling.vertexParity
CDCLean.F₂ is a prerequisite of CDCLean.CubicLabeling.vertexParity
CDCLean.Gamma is a prerequisite of CDCLean.CubicLabeling.vertexParity
CDCLean.GammaFlow is a prerequisite of CDCLean.CubicLabeling.vertexParity
CDCLean.pairIndicator is a prerequisite of CDCLean.CubicLabeling.vertexParity
CDCLean.CubicGraph.edgeAt is a prerequisite of CDCLean.CubicLabeling.vertexParity
CDCLean.CubicLabeling.base is a prerequisite of CDCLean.CubicLabeling.vertexParity
CDCLean.GammaFlow.val is a prerequisite of CDCLean.CubicLabeling.vertexParity
CDCLean.CubicGraph is a prerequisite of CDCLean.GammaFlow.val
CDCLean.Gamma is a prerequisite of CDCLean.GammaFlow.val
CDCLean.GammaFlow is a prerequisite of CDCLean.GammaFlow.val
CDCLean.CubicGraph is a prerequisite of CDCLean.cubic_even_double_cover._proof_2
CDCLean.F₂ is a prerequisite of CDCLean.cubic_even_double_cover._proof_2
CDCLean.Gamma is a prerequisite of CDCLean.cubic_even_double_cover._proof_2
CDCLean.GammaFlow is a prerequisite of CDCLean.cubic_even_double_cover._proof_2

Finish Lean verification

Lean work is attached and awaits signed verification. TheoremDB Researcher can continue from the current declarations and pinned world.

Continue in TheoremDB Researcher

The prefilled request prepares the exact target and checks the current work. It submits an accepted proof and polls verification through any packet-review handoff.

1References

Packet source. OpenAI, A Proof of the Cycle Double Cover Conjecture, preprint (July 2026). Theorem 1.1 and Statement of AI use, page 1; proof, pages 1-3. ↗preprint · primary source · July 2026 · checked 2026-08-01Source use: original summary.States the theorem, gives the proof, attributes the result to GPT-5.6 Sol Ultra, and credits Codex with GPT-5.6 Sol for the writeup.Also cited at Theorem 1.1 and Section 2, pages 1-3, cross-checked against the expositions by Geelen and Oum.Source used to formulate or check the problem record.States and proves the theorem, attributes the conjecture to W. T. Tutte, Alon Itai, Michael Rodeh, George Szekeres, and Paul D. Seymour, credits GPT-5.6 Sol Ultra with the proof, and credits Codex with GPT-5.6 Sol for the writeup.Source named by the research packet.
Sang-il Oum, A proof of the cycle double cover conjecture by OpenAI: An exposition, arXiv:2607.16356v2 (2026). Abstract and full exposition. ↗preprint · independent check source · v2 · checked 2026-08-01Source use: original summary.Independent human exposition of the proof with accessibility modifications.
Jim Geelen, OpenAI's proof of the Cycle Double Cover Theorem, arXiv:2607.15399v1 (2026). Abstract and full exposition. ↗preprint · independent check source · v1 · checked 2026-08-01Source use: original summary.Independent human exposition intended to clarify the proof.
Boris Alexeev and Cheuk Hei Chu, cdc-lean, OpenAI, commit 577e9d9ea326d520f80672ee69b830bf1d513df5 (2026). CDCLean/Main.lean, theorem cycleDoubleCover_of_bridgeless; VERIFICATION.md. ↗software · software source · 577e9d9ea326d520f80672ee69b830bf1d513df5 · checked 2026-08-01Source use: citation only.Pinned Lean 4.31.0 formalization and upstream verification record.Also cited at CDCLean/Main.lean, theorem cycleDoubleCover_of_bridgeless; VERIFICATION.md; contributor commits.Also cited at CDCLean/Main.lean theorem CDCLean.cycleDoubleCover_of_bridgeless and VERIFICATION.md.
François Jaeger, A Survey of the Cycle Double Cover Conjecture, in Cycles in Graphs, North-Holland Mathematics Studies 115 (1985), 1-12. Survey; Proposition 4 for the cubic reduction. ↗proceedings article · reference sourceSource use: original summary.Historical background and the standard reduction to loopless cubic graphs.
Alon Itai and Michael Rodeh, Covering a Graph by Circuits, in Automata, Languages and Programming, LNCS 62 (1978), 289-299. Problem attribution and early formulation. ↗proceedings article · reference sourceSource use: citation only.One of the independent historical formulations credited by the proof paper.
George Szekeres, Polyhedral Decompositions of Cubic Graphs, Bulletin of the Australian Mathematical Society 8 (1973), 367-387. Page 367 and conjecture attribution. ↗journal article · reference sourceSource use: citation only.Historical formulation and the 3-edge-colourable cubic case.
Paul D. Seymour, Sums of Circuits, in Graph Theory and Related Topics, Academic Press (1979), 341-355. Conjecture attribution. ↗proceedings article · reference sourceSource use: citation only.Historical formulation credited by the proof paper.

Original CC0 restatement prepared by TheoremDB after checking the public proof, two independent human expositions, and the pinned Lean repository.

1Context

2Problem setup

3What counts as a solution

1The answerSupportednot Lean-verified

1Records

2See also

1Lean verification

Run the pinned source

1References

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Related work

Record & provenance