Papers With

← All papers
First page of The Borowiecki-Broere Generalized Total Coloring Conjecture for Planar Graphs

The Borowiecki-Broere Generalized Total Coloring Conjecture for Planar Graphs

James Alexander Schreib

math.CO Sep 7, 2026 · v1
formalization mathlib combinatorics
Read PDF arXiv abstract Code
TL;DR
The main theorem is formalized in Lean 4 with Mathlib, conditional on six named axioms including the Four Color Theorem and matroid partition, with a public artifact.
Abstract
We prove the conjecture of Borowiecki and Broere that every finite simple planar graph admits a generalized total coloring with four colors: a proper vertex coloring with four colors together with an edge coloring with four colors in which each edge color class is a forest and no edge receives the color of either endpoint. In fact every proper four-coloring of such a graph extends to an edge coloring of the required kind. The proof combines a component-count inequality for planar graphs whose vertices are partitioned into four independent sets, obtained by completing to a triangulation, with the matroid partition theorem applied to four graphic matroids. A Lean 4 formalization relative to six named background assumptions is described below.
Problem

Borowiecki and Broere conjectured that every finite simple planar graph has a generalized total coloring with four colors. Such a coloring pairs a proper vertex 4-coloring with an edge 4-coloring in which each edge color class is a forest and no edge gets an endpoint's color.

Approach

The proof shows that every proper 4-coloring extends to such an edge coloring. It establishes a component-count inequality for planar graphs partitioned into four independent sets by completing to a triangulation and deleting added edges. Matroid partition applied to four graphic matroids then yields the edge coloring. The argument is formalized in Lean 4 with Mathlib relative to six custom axioms, verified with #print axioms audits and no sorry.

Results

The conjecture is proved for all finite simple planar graphs, in the stronger extension form. The Lean development, partly written with AI assistance, builds with pinned Lean 4.30.0 and Mathlib and is publicly available.