发表机构
New York University（纽约大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文证明了每个有限简单平面图均存在四色广义全染色，即正常四顶点染色可扩展为四色森林边染色，且边色异于端点色，证明结合三角剖分计数不等式与拟阵划分定理，并给出 Lean 4 形式化。
AI 中文摘要
我们证明了 Borowiecki 和 Broere 的猜想：每个有限简单平面图都允许一种具有四种颜色的广义全染色：一种具有四种颜色的正常顶点染色，以及一种具有四种颜色的边染色，其中每个边色类是一棵森林，且没有边获得其任一端点的颜色。事实上，这种图的每个正常四染色都可以扩展为所需类型的边染色。该证明结合了一个平面图的连通分量计数不等式（其顶点被划分为四个独立集，通过补全为三角剖分获得），以及应用于四个图形拟阵的拟阵划分定理。下文描述了相对于六个命名背景假设的 Lean 4 形式化。
英文摘要
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.
Comments6 pages. Lean 4 formalization relative to six named background assumptions available at https://github.com/jamesschreib/borowiecki-broere-conjecture
