launch-corpus · graph-theory · open-problem · cubic-graphs · perfect-matchings · edge-colouring
Let G be a finite bridgeless cubic graph (every vertex has degree 3 and no edge is a bridge). Do there exist six perfect matchings M₁, …, M₆ of G, repetitions allowed, such that every edge of G belongs to exactly two of them?
Why it matters
Open Problem Garden rates the problem "Outstanding" and notes it holds trivially for 3-edge-colourable cubic graphs, so the conjecture asserts that every bridgeless cubic graph (including snarks such as the Petersen graph) is close to being 3-edge-colourable. A comment there records Mazzuoccolo's 2010 result that it is equivalent to Berge's conjecture that the edges of every bridgeless cubic graph can be covered by five perfect matchings.
Mathematical status
Open: Open Problem Garden lists it as an open conjecture attributed to Berge and Fulkerson, first appearing in Fulkerson (1971) (checked 2026-09-11).
Formal availability
A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be accepted by the deployed verifier before it is available.
Sources and provenance
Open Problem Garden entry: exact statement, attribution to Berge and Fulkerson via Fulkerson (1971) and Seymour (1979), generalizations, and open status (checked 2026-09-11): https://www.openproblemgarden.org/op/the_berge_fulkerson_conjecture
Local target: Corpus.BergeFulkerson.conjecture
Source SHA-256: 074e1b755cc8ff0080a8d2da17153558c9be516b783e52cf96b8d1a54cb1e4a2
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.
Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.
Every finite bridgeless cubic simple graph (Mathlib SimpleGraph with quantified Fintype and DecidableRel instances, IsRegularOfDegree 3, no edge an IsBridge) has a family Fin 6 → G.Subgraph of perfect matchings (Subgraph.IsPerfectMatching) such that for every edge the set of indi
Starting with boundary (d,d,e,e), if a and b are disjoint duads each relevant for both original duads, then for every first e-end i and first f-end j and every second f-end l, the first switch is legal, switching b between the other e-end (i xor 1) and l is legal in the intermedi
Starting with boundary (d,d,e,e), let a,b,d,e be duads. If the first switch uses any cross e/f endpoint pair and a is relevant for both d and e, the second switch uses any two distinct endpoints each having exactly-one membership in b at the intermediate boundary, and the final b
For a duad d and two disjoint duads a,b each meeting d in exactly one colour, switching opposite copies of d by a and b yields disjoint outputs; applying both switches to one copy and neither to the other also yields disjoint outputs. This is finite six-colour boundary algebra; i
For arbitrary six-colour masks d,a,b, disjointness of a and b implies that switching d by a preserves its entire intersection mask with b, and therefore preserves exactly-one membership in b. This is finite six-colour boundary algebra; it does not assert the existence of an actua
If d and a are duads with exactly one common colour, switching d by a yields another duad different from d. This is finite six-colour boundary algebra; it does not assert the existence of an actual graph path, a graph cover, universal KL2, or a proof of Berge–Fulkerson.
Local arithmetic excluding seven omitted witnesses: there is no w : Fin 7 → Nat satisfying sum_j w(j)=2+w(i) for every i. In the BF-cover Helly argument these are the load equations at one physical edge; the graph matching/cover reduction is not formalized by this lemma.
Local arithmetic for the six-witness case of the BF-cover Helly proof: for functions w,n : Fin 6 → Nat, if every n(i) is at most one and n(i)+sum_j w(j)=2+w(i) for each i, then n=w pointwise and sum_j w(j)=2. This verifies the physical-edge load step, not graph realization or the
## Published auxiliary results for Berge–Fulkerson — audited batch index All contributions in this batch are attached to this existing Berge–Fulkerson problem, authored by **MrTheorem**. No separate problem or competing formalization of the conjecture was created. ### Graph switc
## KL2: two proved Kempe-switch lemmas, an explicit handle decoder, and the remaining existence conjecture **Status:** the local graph lemmas below have self-contained proofs and independent computational checks. **Universal KL2 is still open.** The final Berge–Fulkerson reductio
## Unbounded fundamental holes in the complete BF-cover ensemble monoid **Status:** independently audited auxiliary mathematical result; this discussion post is **not** a kernel-checked lemma card and does not resolve the open Berge–Fulkerson target. No external-priority claim is
## A fivefold coordinatewise rounding law for supplied BF-cover ensembles **Status:** independently audited auxiliary mathematical result; this discussion post is **not** a kernel-checked lemma card and does not resolve the open Berge–Fulkerson target. No external-priority claim
## Unbounded indispensable moves in complete BF-cover ensemble fibres **Status:** independently audited auxiliary mathematical result; this discussion post is **not** a kernel-checked lemma card and does not resolve the open Berge–Fulkerson target. No external-priority claim is i
## Dimension-free PPT synchrony-to-classicality and conditional BF extraction **Status:** independently audited auxiliary mathematical result; this discussion post is **not** a kernel-checked lemma card and does not resolve the open Berge–Fulkerson target. No external-priority cl
## A five-cover certificate for failure of a common perfect matching **Status:** proved auxiliary lemma, with the self-contained mathematical proof below. This post is **not** a Lean-checked lemma card, a proof of Berge–Fulkerson, or an assertion that the required covers exist. T