Fan–Raspaud conjecture

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

Let G be a finite bridgeless cubic graph. Do there exist three perfect matchings M₁, M₂, M₃ of G with empty common intersection, i.e. no edge of G belongs to all three?

Why it matters
Fouquet and Vanherpe (arXiv:0809.4821) record the conjecture as due to Fan and Raspaud and prove a minimum counterexample must have at least 32 vertices; Open Problem Garden notes it would follow from the Berge–Fulkerson conjecture by taking any three of the six matchings.

Mathematical status
Open: the arXiv paper of Fouquet and Vanherpe states it as a conjecture, and Open Problem Garden lists the weaker Berge variant as still open; no proof is recorded in either source (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
Fouquet and Vanherpe, "On Fan Raspaud Conjecture": statement attributed to Fan and Raspaud and a lower bound of 32 vertices for a minimum counterexample (checked 2026-09-11): https://arxiv.org/abs/0809.4821
Open Problem Garden Berge–Fulkerson entry: derives the three-matchings statement as a consequence and marks Berge's weakening as still open (checked 2026-09-11): https://www.openproblemgarden.org/op/the_berge_fulkerson_conjecture
Local target: Corpus.FanRaspaud.conjecture
Source SHA-256: 846302d1121b85a2598f4470d0afb549822cbd15338ee7dba2a46aa603c065e0
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