The four color theorem, proved in 1976, says that any map (or planar graph) can be colored with just four colors so that no two neighboring regions share a color. A related but harder question asks whether you can simultaneously color both the vertices and the edges of a planar graph using only four colors, subject to certain rules. Borowiecki and Broere conjectured that this is possible, where the edge coloring must satisfy two conditions: each color class of edges forms a forest (no cycles), and no edge can receive the same color as either of its two endpoints. This paper proves that conjecture.
The proof works in two main steps. First, the authors take any valid four-coloring of the vertices and analyze the structure of the graph by completing it to a triangulation, which allows them to count connected components in a useful way. This gives them a numerical inequality relating the structure of the graph to the number of available colors. Second, they use a classical result from matroid theory called the matroid partition theorem, which is a powerful tool for deciding when a collection of edges can be split into pieces with desired properties. Combining these two ingredients shows that the required edge coloring always exists on top of any valid vertex coloring.
The paper also includes a formal computer-verified proof of the result written in a proof assistant language called Lean 4, which checks every logical step mechanically. This formalization relies on six explicitly stated background assumptions, meaning the computer has verified the argument is airtight given those foundations. The result is notable both as a resolution of a longstanding open conjecture and as an example of combining combinatorial geometry, matroid theory, and computer-assisted verification to settle a problem in graph coloring.