院士论坛回顾｜数学科学学院第44期院士论坛

2026年9月29日下午，复旦大学数学科学学院第44期院士论坛在光华楼东辅楼103室举行。加拿大西蒙菲莎大学杰出教授Bojan Mohar带来题为 《The Four Color Theorem: The Tip of the Iceberg》的专题报告。报告以经典的四色定理为起点，从可人工核查的证明、算法以及相关推广等多个角度，带领大家探寻四色定理这一“冰山一角”背后更为丰富的图论结构与问题。本次报告由数学科学学院院长沈维孝院士主持。

报告的第一部分，Mohar教授回顾了四色定理的发展历史。四色定理源于19世纪中叶的地图着色问题，其后经历了多次证明尝试，并最终在1976年由Appel和Haken借助计算机完成证明，1996年 Robertson、Seymour、Sanders 和 Thomas 又对证明进行了重要改进。Mohar教授进一步介绍了Tait关于三次平面图边着色的等价表述，以及Tutte建立的着色与流之间的对偶关系：平面图的顶点着色问题可以转化为其对偶图上的nowhere-zero flow问题。由此，四色定理不再只是一个孤立的地图着色结论，而与边着色、网络流及更一般的图结构自然联系起来。

报告的第二部分，Mohar教授聚焦四色定理的深层证明逻辑与可核查优化方法。Mohar教授主要讲解了四色定理核心证明工具，涵盖可约构型、Kempe交换、放电法及不可避免集的构造思路。针对传统证明的局限，团队重点优化了零曲率平坦区域的处理方式，证实平面图中广泛存在可约结构。同时，研究团队将证明场景归约至5-sparse图，精简了放电规则与可约构型数量，搭建起简洁透明的证明框架。该研究还证实平面三角剖分存在大量独立可约结构，不仅深化了对四色定理的核心认知，也实现了平面图四色着色的近线性时间高效算法。

报告的第三部分，Mohar教授向我们展现了四色定理这一“冰山一角”之下的广阔研究图景。Mohar教授将研究视野从传统平面图延伸至射影平面、环面等各类曲面图形，同时结合Albertson猜想、强4-flow定理、apex图等前沿研究，阐释了Tutte流猜想相关的广义图类研究进展。他指出，四色定理绝非单一的经典结论，而是图论研究的重要入口，其衍生的曲面图研究、流理论、边着色算法等方向，仍是当前图论领域持续深耕、不断迭代的核心研究领域。

此外，Mohar教授还专门介绍了计算机与人工智能在证明中的作用。计算机可承担构型检验、批量验证等大量繁复的机械性工作，但他特别强调，AI并未被用于获得此次报告所介绍的数学证明。团队主要借助AI辅助编程，由AI生成并运行验证程序，再与人工设计的计算结果相互比对，为结论的准确性增加了一层独立复核保障。

在报告后的互动提问环节，在场师生围绕 5-sparse 情形下的可人工核查证明、零曲率“平坦区域”的处理、放电规则如何寻找以及人工智能未来可能如何参与数学研究等问题踊跃提问。Mohar教授结合报告内容逐一作了回应。他指出，放电规则的寻找目前并不存在一个完全机械化的办法，虽然线性规划等工具可能提供一定帮助，但研究过程中仍需要依靠数学直觉，不断尝试规则、分析反例，并在新的可约构型与新的放电规则之间反复调整。谈及AI对数学证明的影响时，他表示，数学研究的目标不仅在于知道一个命题“是真的”，更重要的是理解它“为什么是真的”；计算机和AI可以帮助数学家承担越来越多机械性的工作，但对于数学结构及其背后原因的理解，仍然是研究中不可替代的重要部分。