在四维空间中，七块总是够用

取一个形状——任意一个有界的点集——把其中两点之间的最大距离称为它的直径。现在把它切成若干块，使每一块都严格比整体窄。无论形状如何，总能奏效的最少块数是多少？

在n维空间中，这个数被称为博尔苏克数（Borsuk number）b_n。1933年，博尔苏克（Borsuk）提出疑问：它是否总等于n + 1？它不可能更小：正单形的顶点——平面上的正三角形、空间中的正四面体——需要n + 1块，因为任意两个顶点之间的距离都恰好是一整个直径。而在一维、二维和三维空间中，n + 1块都够用。1993年，卡恩（Kahn）和卡莱（Kalai）证明，在维数足够高时这个猜想不成立。

第一个悬而未决的情形

四维是第一个无人知道答案的情形。拉萨克（Lassak）给出的一个古老的一般上界2ⁿ⁻¹ + 1，在四维时意味着最多九块。2026年早些时候，托尔马乔夫（Tolmachev）和沃罗诺夫（Voronov）借助计算机辅助构造，把它降到了八块。

曼尼托巴大学的A. Arman和A. Prymak、挪威科技大学的A. Bondarenko，以及法国高等科学研究所（Institut des Hautes Études Scientifiques）的D. Radchenko，现在证明了一个更强的命题。四维空间中每一个直径为1的集合，都可以被七个直径相同、且严格小于0.9999的球覆盖。每个球都比该集合窄，因此把每个点分配给其中一个球，就把集合切成了七个更窄的块：b₄ ≤ 7。答案现在介于五和七之间。

从最小外接球出发

证明从外接球（circumball）开始：即包含该集合的最小的球。荣格（Jung）的一条经典定理限制了它的大小——对于直径为1的集合，其半径至多约为0.63（半径的平方至多为2/5）。集合与外接球的球面相接触，在这些接触的点中，最多五个就足以把球固定住；作者称之为接触点。这些点约束了集合其余部分可能的位置，因为没有任何点与其中任何一个接触点的距离超过1。

接着，作者按外接球的大小把问题分为三种情形：

• 外接球较小：七个按固定的明确方式排列的球覆盖整个外接球，无论其中的集合是什么。这一点通过手工证明。
• 外接球较大：此时有五个接触点。五个球，各自的球心位于从中心到某个接触点的路程的9/20处，几乎覆盖了一切；另外两个球覆盖剩下的部分，即两个锥形区域。同样通过手工证明。
• 介于两者之间：构成锐角三角形的三个接触点，把每一种可能的集合都归结为一族只需四个数就能描述的形状。计算机正是在这里登场。

23494个方框，没有舍入

这四个数构成一个由各种可能性组成的四维立方体。对于这个立方体中的每个小方框，先由数值搜索提出七个球心。然后用一项精确检验，确认这同样的七个球覆盖了方框内的每一个形状。

其中的技巧是计算几何中的一个经典手法：增加第五个坐标，令其等于到原点距离的平方，就能把“在这个球内”和“在那个球外”变成线性不等式。问题于是变成：由十二个这样的不等式切出的多胞形（一种由平面围成的形状），是否完全位于一个弯曲的碗面之上——而要判断这一点，只需检查它的顶点。程序检查了全部792个候选顶点，只使用整数和精确分数，不设任何数值容差。

如果某个方框未通过检验，就把它一分为二，两半分别重新检验。最终，这个立方体被切成了23494个方框，最多经过29层对半切分，而每一个都通过了检验。它们的体积加起来恰好为1：没有任何遗漏。数据和验证程序均已公开。作者指出，该程序使用精确算术，但并不是经由证明助手核查的形式化证明。

思路从何而来

作者坦率地讲述了他们是如何走到这一步的。他们早先的一个版本只做到了八块，而且需要多得多的计算；当时语言模型只在编写代码方面提供了帮助。后来，他们借助ChatGPT Astra探索这个问题，起初是寻找纯分析的论证。这番探索引出了以外接球为基础的思路，大大缩小了计算机搜索的规模。他们还用ChatGPT编写代码和润色文稿，并亲自核查了每一个数学论证和验证代码。

博尔苏克本人对四维情形的猜测——五块——至今既未被证明，也未被推翻。新的上界距离它还差两步。