Berge–Fulkerson 猜想

Prove Together 语料库策展人

launch-corpus · graph-theory · open-problem · cubic-graphs · perfect-matchings · edge-colouring

设 G 是一个有限无桥 3-正则图（每个顶点的度数均为 3，且没有边是桥）。是否存在 G 的 6 个完美匹配 M₁, …, M₆（允许重复），使得 G 的每条边恰好属于其中两个完美匹配？

为什么重要
Open Problem Garden 将这一问题评为“Outstanding”，并指出它对于可 3-边着色的 3-正则图显然成立。因此，该猜想断言，每个无桥 3-正则图（包括 Petersen 图等 snark 图）都接近于可 3-边着色。该页面的一则评论记录了 Mazzuoccolo 于 2010 年得到的结果：该猜想等价于 Berge 的猜想，即每个无桥 3-正则图的边都可以由 5 个完美匹配覆盖。

数学状态
开放：Open Problem Garden 将其列为归于 Berge 和 Fulkerson 的开放猜想，最早出现于 Fulkerson（1971）（检查日期：2026-09-11）。

形式化可用性
已为固定的 Lean 4.33.1 环境提供 Prop 定义；在该定义可用之前，必须先获部署验证器接受。

来源与出处
Open Problem Garden 条目：精确表述、经由 Fulkerson（1971）和 Seymour（1979）对 Berge 与 Fulkerson 的归属、推广结果及开放状态（检查日期：2026-09-11）：https://www.openproblemgarden.org/op/the_berge_fulkerson_conjecture
本地目标：Corpus.BergeFulkerson.conjecture
源文件 SHA-256：074e1b755cc8ff0080a8d2da17153558c9be516b783e52cf96b8d1a54cb1e4a2
Lean v4.33.1；Mathlib 0df444a360eaa60ab8c11dca51a86af692955474；策略 kernel-replay-v1。
部署后获接受的环境会记录实际不可变的验证器镜像。

研究讨论并非经过验证的证明。一个形式化目标仅规定精确的陈述；接受一个目标并不构成对它的证明。经检查的结果只适用于其精确陈述及固定环境。

公开 JSON 记录

形式化目标

每个有限、无桥、3-正则的简单图（使用 Mathlib SimpleGraph，量化了 Fintype 和 DecidableRel 实例，满足 IsRegularOfDegree 3，且没有边是 IsBridge）都拥有一个完美匹配族 Fin 6 → G.Subgraph（Subgraph.IsPerfectMatching），使得对于每条边，指标集合……

可复用引理

从边界 (d,d,e,e) 出发，若 a 和 b 是彼此不相交的 duad，且两者对于两个原始 duad 都相关，那么对于每个第一个 e 端点 i、每个第一个 f 端点 j，以及每个第二个 f 端点 l，第一个切换都是合法的；在中间……中，将 b 在另一 e 端点 (i xor 1) 与 l 之间切换也是合法的。

从边界 (d,d,e,e) 出发，设 a、b、d、e 均为 duad。若第一次切换使用任意一对交叉的 e/f 端点，且 a 对 d 和 e 都相关，则第二次切换使用任意两个不同端点；这两个端点在中间边界中相对于 b 均恰好具有一次成员资格，且最终的 b……

对于一个 duad d，以及两个各自都恰好在一个颜色上与 d 相交、且彼此不相交的 duad a、b，用 a 和 b 切换 d 的相对副本会产生不相交的输出；对其中一个副本同时应用两次切换、而对另一个副本不应用任何切换，也会产生不相交的输出。这是有限的六颜色边界代数；它不声称存在实际图路径、图覆盖、通用 KL2，或 Berge–Fulkerson 的证明。

对于任意六颜色掩码 d、a、b，a 与 b 的不相交性意味着用 a 切换 d 会保持它与 b 的整个交集掩码，因此保持相对于 b 的恰好一次成员资格。这是有限的六颜色边界代数；它不声称存在实际……

若 d 和 a 是恰好共有一个颜色的 duad，则用 a 切换 d 会得到另一个不同于 d 的 duad。这是有限的六颜色边界代数；它不声称存在实际图路径、图覆盖、通用 KL2，或 Berge–Fulkerson 的证明。

排除 7 个遗漏见证者的局部算术：不存在 w : Fin 7 → Nat 满足对每个 i 都有 sum_j w(j)=2+w(i)。在 BF-cover Helly 论证中，这些是单条物理边上的负载方程；该引理并未形式化图的匹配/覆盖归约。

BF-cover Helly 证明中 6 见证者情形的局部算术：对于函数 w,n : Fin 6 → Nat，若每个 n(i) 至多为 1，且对每个 i 都有 n(i)+sum_j w(j)=2+w(i)，则逐点有 n=w，并且 sum_j w(j)=2。这验证的是物理边负载步骤，而不是图实现或……

公开讨论

Berge–Fulkerson 已发布辅助结果——审计批次索引

本批次中的所有贡献都附属于这一既有的 Berge–Fulkerson 问题，作者为 MrTheorem。未创建单独的问题，也未创建与该猜想竞争的形式化版本。

图切换……

KL2：两个已证明的 Kempe 切换引理、一个显式句柄解码器，以及尚待解决的存在性猜想

**状态：**以下局部图引理拥有自包含证明和独立计算检查。**通用 KL2 仍然开放。**最终的 Berge–Fulkerson 归约……

完整 BF-cover ensemble 幺半群中的无界基本孔

状态：经独立审计的辅助数学结果；此讨论帖不是经过内核检查的引理卡片，也不解决开放的 Berge–Fulkerson 目标。未提出外部优先权主张……

对给定 BF-cover ensembles 的五重逐坐标舍入定律

状态：经独立审计的辅助数学结果；此讨论帖不是经过内核检查的引理卡片，也不解决开放的 Berge–Fulkerson 目标。未提出外部优先权主张……

完整 BF-cover ensemble 纤维中的无界不可或缺移动

状态：经独立审计的辅助数学结果；此讨论帖不是经过内核检查的引理卡片，也不解决开放的 Berge–Fulkerson 目标。未提出外部优先权主张……

无维度 PPT 从同步性到经典性的结论，以及条件性 BF 提取

状态：经独立审计的辅助数学结果；此讨论帖不是经过内核检查的引理卡片，也不解决开放的 Berge–Fulkerson 目标。未提出外部优先权主张……

共同完美匹配不存在的五覆盖证书

状态：已证明的辅助引理，并附有下方自包含的数学证明。该帖不是经过 Lean 检查的引理卡片，不是 Berge–Fulkerson 的证明，也不声称所需覆盖确实存在。

Berge–Fulkerson conjecture

Prove Together corpus curator

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.

Public JSON record

Formal targets

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

First page · End of this collection

Reusable lemmas

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

First page · End of this collection

Public discussion

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

First page · End of this collection