结果族 158：The Euclidean plane cannot be colored with five colors · 学科：Combinatorics · 验证状态：主结果已 Lean 形式化
想象给一整张无限大的地图上色，规则只有一条：距离恰好为 1 的两点不许同色。这篇论文证明：只用 5 种颜色怎么涂都会”撞色”——平面上总有两个相距恰为 1 的点颜色相同。于是这个悬置七十余年的”最少需要几色”问题（Hadwiger–Nelson 问题），答案被压缩到只剩 6 或 7 两个候选。
关键词卡片
@@M@@\chi(\mathbb{R}^2)@@。看个具体例子
先体会规则有多苛刻：边长为 1 的等边三角形，三个顶点两两相距 1，必须占用 3 种不同颜色。
小三角形只需 3 色，但要同时管住全平面的所有单位距离，难度暴涨：六边形铺砖给出 7 色方案，2018 年 de Grey 的构图把下界推到 5，而本文证明 5 色必败，下界升为 6。关键突破是一座”转移定理”之桥：任意（哪怕完全不规则）的染色存在，当且仅当某种弱可测染色存在——可测世界的几何工具由此全线上场，最终由 Moser 主轴这颗小钉子钉死矛盾。
为什么值得关心
平面色数是几何图论最著名的未决问题之一，其下界七十多年来首次移动。
已 Lean 形式化
第一级台阶
入门导读把这问题比作给一张无限大的地图上色。翻译成半数学的语言：对象是平面上的每一个点，操作是给每个点指派五种颜色之一，约束是凡相距恰好一个单位的两个点必须拿到不同的颜色。要问的是：这样的指派方案到底存不存在。
第二级台阶
用本科图论术语说：给每点指定颜色、使每个单位距离点对不同色的方案叫正常染色；完成这件事所需的最少颜色数记作平面色数。可测染色进一步要求每种颜色的点集在勒贝格测度意义下温和可测；弱可测染色则放宽为只要求同色单位点对在乘积测度下测度为零。此前的下界结论大多被锁在可测世界之内。
第三级台阶
主定理在最一般语境下陈述：对任意五染色、不做任何可测性或正则性假设，必存在同色单位点对。证明的两大块假设各自挡住一类麻烦：转移定理挡住”颜色集完全不规则、无密度点结构可用”，把任意染色化归为弱可测染色；几何障碍部分挡住”弱可测世界里残余的五染色”，用调色板与标签圈分析把矛盾推到 Moser 主轴不可三染色这一经典事实上。结论：平面色数被夹在六与七之间，七十余年的候选从五个砍到两个。
本文无条件证明：欧氏平面的任意五染色必有距离恰为 1 的同色点对，无须对颜色类做任何可测性或正则性假设；于是平面色数 @@M@@\chi(\mathbb{R}^2)@@ 只能是 6 或 7，Hadwiger–Nelson 问题的下界七十多年来首次从 5 跃升至 6。
Hadwiger–Nelson 问题问：把平面上每一点染色，使距离恰为 1 的两点不同色，至少需要几种颜色？答案记作 @@M@@\chi(\mathbb{R}^2)@@，即以全平面为顶点、单位距离点对为边的无限图的色数 (chromatic number)。问题源于 1950 年的 Edward Nelson：他证得下界 4，John Isbell 用六边形染色给出上界 7；Moser 主轴 (Moser spindle) 是经典的 7 点不可三染色障碍图。2018 年 de Grey 构造 1581 个顶点的有限单位距离图把下界提高到 5，随后被精简到 553 与 509 个顶点，但下界 6 始终无人触及。难点在于：若不假设颜色类勒贝格可测 (Lebesgue measurable)，就没有密度点结构可利用——Falconer 1981 年的可测下界 @@M@@\chi_m(\mathbb{R}^2)\ge 5@@ 一直无法推广到任意染色。本文的突破口，正是在”任意染色”与”可测条件”之间架起一座双向桥。
主定理：欧氏平面不存在正常五染色 (proper five-coloring)——任何函数 @@M@@c:\mathbb{R}^2\to\{1,\dots,5\}@@ 必有某对点满足 @@M@@|x-y|=1@@ 且 @@M@@c(x)=c(y)@@。结合经典的六边形七染色构造，得 @@M@@6\le\chi(\mathbb{R}^2)\le 7@@，剩余的 6 与 7 两种可能仍未决。
证明分两半。其一是转移定理 (transfer)：对每个有限 @@M@@k@@，”存在正常 @@M@@k@@-染色”当且仅当”存在弱可测 @@M@@k@@-染色 (weak measurable coloring)”——即可测函数 @@M@@c:\mathbb{R}^2\to\{1,\dots,k\}@@，其色类 @@M@@A_i@@ 满足对每个 @@M@@R>0@@ 都有 @@M@@\sum_i\int_{B(0,R)}\int_{S^1}\ind_{A_i}(x)\ind_{A_i}(x+u)\,d\sigma(u)\,dx=0@@，即乘积测度意义下几乎没有同色单位点对。其二是：不存在弱可测五染色。由此还得到概率性推论：存在常数 @@M@@\delta>0@@，使任何五染色在不变平均意义下同色单位点对的频率至少为 @@M@@\delta@@（@@M@@\delta@@ 可取某个不可五染的有限图边数的倒数）。
全文分”转移”与”几何障碍”两大块。先做转移：把正常染色限制在可数的代数平面 @@M@@E=F(i)@@（@@M@@F@@ 为实代数数域）上，对可解群 @@M@@E\rtimes K@@（@@M@@K@@ 为代数单位旋转群）作 Følner 平均，得到平移旋转不变的概率律，每个标签指示函数 @@M@@f_i@@ 满足 @@M@@\int f_i\,T_uf_i\,d\mu=0@@。再用谱定理把 @@M@@f_i@@ 分成连续特征子群 @@M@@C@@ 支撑的部分 @@M@@p_i@@ 与正交余部 @@M@@b_i@@；关键工具是 Haar 刚性定理 (rigidity)：在 @@M@@E@@ 的紧特征群 @@M@@D@@ 上，任何 @@M@@K@@-不变且避开 @@M@@C@@ 的概率测度必为 Haar 测度。其证明借助 Furstenberg–Zimmer 紧扩充方法构造因子塔，相对奇异性引理保证条件差分布仍避开 @@M@@C@@，两条代数单位方向的恒等式导出径向 Fourier 系数的差不等式，最后用数域中”有理一般位置”的有限论证把该系数在一切非零半径上压为零。于是余部 @@M@@b_i@@ 与它的每个非零代数平移正交，删去它不破坏单位距离排斥；@@M@@p_i@@ 非负、坐标和为 1，平移算子还能连续延拓到整个 @@M@@\mathbb{R}^2@@，取一个可测样本、逐点选最小正坐标标签，即得弱可测染色。反方向则用密度点：弱色类的满密度点集不含单位点对（Falconer–Payne 机制的推广），再由 de Bruijn–Erdős 图紧性 (compactness) 复原正常染色。
再做几何障碍：先在固定中心 @@M@@x@@ 处对典型角度采样取弱-*极限，得到调色板 (palette)，并证明几乎处处至多含两个标签；标签间的转移图仅在闭的局部有限中心集 @@M@@\mathcal L@@ 上含圈，圈外是森林。接着把色指示函数作圆盘平均再阈值化，得到取值于五标签完全图的连续映射，小洞用树填充；一个 Brouwer 不动点式的覆盖障碍迫使某个核心盘的边界环非零伦，其约化词给出长度 @@M@@\ell\in\{3,4,5\}@@ 的简单标签圈，每条边中点原像的连通分量横穿环带，取 Hausdorff 极限得到共享点 @@M@@x@@ 的紧连通集 @@M@@K_j@@，且两个端点标签的本质支撑都避开跨立区域 @@M@@\Delta(K_j)=\{z:\min_{q\in K_j}|z-q|<1<\max_{q\in K_j}|z-q|\}@@。最后用 @@M@@K_j@@ 逼近 @@M@@x@@ 的极限方向区分单位圆内、外侧的允许标签：五圈与六位置角字矛盾，四圈与对径方向的奇偶规则冲突，三圈迫使六个 @@M@@\pi/3@@ 扇区交替、留出一个几乎处处只用三个圈标签的开区域；显式有理放置证书把 Moser 主轴的七个顶点全部放入该区域，而 Moser 主轴不可正常三染色，矛盾完成证明。
按任务标注，主结果已获 Lean 形式化证明（家族文档 lean/docs/158.md），这是当前最强的可信度信号；论文在 ZFC 内写作，Moser 放置的有理证书一节给出完全可人工复核的严格不等式验证。本结果与经典七染色上界合并，把 Hadwiger–Nelson 问题压缩到 @@M@@\chi(\mathbb{R}^2)\in\{6,7\}@@；论文脚注还指出 2026 年 5 月另一宣布 @@M@@\chi(\mathbb{R}^2)=7@@ 的稿件中，关键的角密度界 @@M@@\pi/3@@ 存在半开弧反例，故 6 与 7 之争仍开放。按 OpenAI 官方声明，”未经形式化的结果可能有问题”，读者宜以形式化仓库与社区核验为准。
问 1：证明里最关键、也最脆弱的一步在哪里？
答：转移定理中”删去谱余部后不破坏单位距离排斥”一步。它先把染色限制在可数代数平面上做 Følner 平均，再用 Haar 刚性定理把余部与一切非零代数平移的正交性压到所有非零半径；两条代数单位方向的恒等式若有一处系数差错，矛盾就可能悄悄失效，后续几何部分全部落空。
问 2：为什么必须绕开可测性假设，不能直接套 Falconer 的老路？
答：Falconer 1981 年的 @@M@@\chi_m\ge 5@@ 依赖密度点论证，只对可测染色成立；任意染色可以出现完全不可测的色集，那里没有任何密度结构。本文转移定理的价值正是把无正则性情形双向化归到弱可测世界，可测世界的几何工具才得以全线上场——这是它与前人所有下界工作的本质分野。
问 3：与 2018 年 de Grey 的下界 5 相比，真正的新意是什么？
答：de Grey 靠一张 1581 顶点的显式有限单位距离图，计算机可验但只能到 5。本文新在”无限对有限”的双层结构：先用遍历论与谱方法排除一切（含不可测）五染色，矛盾最后收口在 Moser 主轴这张仅 7 个顶点的经典小图上，并附可人工复核的有理放置证书。
问 4：这类 AI 参与生成的证明最可能在哪里出错？
答：角分析端点。论文自己的脚注就指出，2026 年 5 月另一篇宣布 @@M@@\chi=7@@ 的稿件正是在 @@M@@\pi/3@@ 角密度界上败于半开弧反例；本文标签圈与扇区交替的论证同样在最敏感的区间工作，属于最该逐行核验之处。所幸主结果已另附 Lean 形式化证明，风险有兜底。
问 5：为什么最后出场的是 Moser 主轴，而不是更大的障碍图？
答：几何部分先把弱可测五染色压缩到某个开区域几乎处处只用三个圈标签，于是在该区域内任何一个不可三染色的单位距离图都足以引爆矛盾；主轴最小最经典，其七点放置的有理不等式证书反而成了全文最透明的部分。
问 6：这个结果谁会用？下一步是什么？
答：一切关心 @@M@@\chi(\mathbb{R}^2)@@ 是 6 还是 7 的人——无论造六染色构造还是证七色下界，都必须先穿过本文的转移定理。论文未展开向高维欧氏空间或一般度量平面的推广，也未给出概率性推论中常数 @@M@@\delta@@ 的具体数值。
总评
这是 Hadwiger–Nelson 问题七十余年来下界的首次实质移动，且有形式化背书，分量十足；最大风险集中在转移定理的谱-刚性细节与角分析端点处理，宜以 Lean 仓库与社区核验为最终裁判。