OpenAI 把平面色数下界提到 6，Lance 撰文解析证明思路

OpenAI 声称把单位距离图着色问题的平面色数下界从 5 提到 6，即 6≤χ，并已在 Lean 中形式化。该证明不是搜索更大的图，而是先证明若存在正常 5-着色则存在弱可测正常 5-着色，再证明不存在弱可测正常 5-着色以推出矛盾。计算复杂性博主 Bill Gasarch 撰文评论了这一结果，并新增网站汇总 OpenAI 宣称解决的一批理论计算机科学和数学猜想。