AI破解一道着色难题
取一个由线连接的点组成的网络——数学家称之为图。现在给这些点着色，使任何两个由线相连的点颜色都不相同。能做到这一点的最少颜色数，就是这个图的色数。一个著名的特例是1977年被证明的四色定理，其标题已说明一切：“Every planar map is four colorable”（每张平面地图都可以四色着色）。
哈德维格1943年的猜想
1943年，哈德维格（Hadwiger）为所有图提出了一条普适规则。通过删除点或线，以及把两个相连的点合并为一个点，来缩小一个图。所得结果称为子式（minor）。哈德维格关注的是以这种方式能得到的最大完全图——其中每个点都与其他所有点相连的团——并猜想所需颜色数永远不会超过这个团的大小。
论文称之为“图论中最古老、最基本的问题之一”。它只在较小的情形下被证明：团的大小不超过5时，它被证明等价于四色定理或可归结为四色定理。从6开始，问题仍未解决。
一个对数一个对数地逼近
由于精确表述难以攻克，研究者们试图用团大小的某个增长尽可能缓慢的函数来界定颜色数。论文回顾了相关进展。几十年来，最好的上界增长得比正比例略快一些——多出一个涉及对数平方根的因子。几年前，Norin、Postle和Song打破了这一壁垒。Delcourt和Postle随后进一步改进，并且关键地证明了只需处理相当小的图即可。Liu和Luo把额外因子压低到三重对数。
自然的终点是线性哈德维格猜想：团大小的某个固定倍数总是足够的。这正是蒙特利尔麦吉尔大学的Sergey Norin和苏黎世联邦理工学院的Raphael Steiner如今声称已经证明的结论。
机器扮演的角色
作者说得很明确：**证明是由OpenAI的模型GPT-6 Astra按照他们的指示找到的。**他们首先请它证明非常稠密图的情形，他们认为这正是缺失的一块。他们写道，它“仅用了几个小时，再加上一些鼓励”就成功了。当被要求把某个依赖关系写成显式形式时，它覆盖了一定规模以内的图——但没有完全达到所需的范围。于是他们请它提出一个原创想法来弥补这一缺口，由此产生了最终证明中的“自举”（bootstrap）步骤。他们说，除了一个关于收缩的建议外，作者自己具体的证明思路几乎都没有保留下来。
文字由人类撰写。另一个OpenAI模型协助了校对和参考文献整理。作者报告说，OpenAI的Codex在证明助手Lean中生成了整个证明的形式化、可由机器检验的版本，并与一份早期由AI撰写的草稿一起发布在网上。他们对其中的数学内容承担全部责任。
证明的内部结构
论证分为两半：
- 小图，少颜色。对于规模不比团大小上限大很多的图，作者证明大约4倍的团大小就足够。出发点是Reed和Seymour在1998年的一个结果：一种放宽的“分数”着色已经满足因子为2的线性规则。新工作通过向图中添加少量额外的线，并在一个辅助结构中找到巨大的匹配，把分数着色转化为真正的着色。
- **自举。**第二个论证在每一步把所覆盖的图规模范围在指数上扩大三分之四倍，代价是常数变大。十步之后，范围从三分之一扩展到约5.92，超过了Delcourt-Postle归约所要求的阈值5。这一半用到了Gyárfás的一个老技巧，作者说它此前从未被应用于这个问题。
作者把这个证明描述为由已知工具构建而成——“包含在现有结果的凸包之内”，但并不位于其显而易见的边缘上。
仍然悬而未决的问题
这个常数极其巨大：粗略估计约为10¹⁰⁰。作者认为有空间把它降到10¹⁰以下，但认为要降到比如100，就需要新的想法。哈德维格的原始猜想则丝毫未动：“我们尚无定论，“他们写道。这篇论文是预印本；41页新的数学内容现在将接受其他专家的审视。