A Lean 4 formalization project invites collaborative proof attempts for the Berge–Fulkerson conjecture, an outstanding open problem asserting that every bridgeless cubic graph admits six perfect matchings covering each edge exactly twice. The conjecture, attributed to Berge and Fulkerson (1971), is known to hold for 3-edge-colorable graphs and relates to broader questions about edge coloring in cubic graphs.