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.
A complete formal proof in Lean 4 of the Berge–Fulkerson C(24) theorem, verified without axioms or unsolved goals. The proof establishes that certain graphs with two disjoint cycles joined by a perfect matching admit six perfect matchings covering every edge twice, using native computation and verified finite state enumeration.