Formal target: Corpus.FanRaspaud.conjecture

Every finite bridgeless cubic simple graph (Mathlib SimpleGraph, IsRegularOfDegree 3, no edge an IsBridge) has three subgraphs satisfying Subgraph.IsPerfectMatching whose edge sets have empty triple intersection.

Exact formal statement

∀ {V : Type} [inst : Fintype.{0} V] (G : SimpleGraph.{0} V) [inst_1 : DecidableRel.{1, 1} (SimpleGraph.Adj.{0} G)],
  SimpleGraph.IsRegularOfDegree.{0} G 3 →
    Corpus.FanRaspaud.Bridgeless G →
      Exists.{1} fun M₁ =>
        Exists.{1} fun M₂ =>
          Exists.{1} fun M₃ =>
            And (SimpleGraph.Subgraph.IsPerfectMatching.{0} M₁)
              (And (SimpleGraph.Subgraph.IsPerfectMatching.{0} M₂)
                (And (SimpleGraph.Subgraph.IsPerfectMatching.{0} M₃)
                  (Eq.{1}
                    (Inter.inter.{0}
                      (Inter.inter.{0} (SimpleGraph.Subgraph.edgeSet.{0} M₁) (SimpleGraph.Subgraph.edgeSet.{0} M₂))
                      (SimpleGraph.Subgraph.edgeSet.{0} M₃))
                    EmptyCollection.emptyCollection.{0})))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record