一个积木块，没有算法

取几个小立方体，把它们面对面粘成一个积木块——即一个多立方体（polycube）。现在问：这个积木块的复制品只能移动、永远不能旋转，能否无缝隙、无重叠地填满整个空间？

这听起来像是计算机靠穷举就能解决的问题。麻省理工学院的Erik Demaine和布鲁塞尔自由大学的Stefan Langerman证明，一般而言，这是做不到的。没有任何算法能够针对每一个多立方体判定它能否铺满三维空间。这个问题是不可判定的。

漫长的倒计时

不可判定的铺砌问题有着悠久的历史，论文对此做了回顾。起点是王氏砖（Wang tiles）问题——每条边都有一种颜色的正方形，摆放时相接的边颜色必须一致。1966年，有人证明了判定一组王氏砖能否铺满平面是不可判定的，但这一结果需要任意多块砖。

从那以后，数学家们一直在倒数：最少需要几种砖的形状，才能让这个问题保持不可判定：

• 在平面上，2009年是11块，2025年降到3块；
• 在空间中，起初是6块，2026年降到2块；
• 而现在，在空间中，只需1块。

维度不能再低了：对于平面上的单块砖，已知这个问题是可判定的。至于平面上的两块砖，答案仍未可知。

积木块里的数独

证明串联了五个构造。它从王氏砖出发，沿用Rachel Greenfeld和陶哲轩（Terence Tao）此前的工作，把它们变成一种无限的数独：在一个网格中，每条给定斜率的直线都必须读作少数几个允许的“单词”之一，其规则建立在两个素数的幂之上。

作者主要的新步骤，是改造OpenAI最近的一个构造——一种能填满空间、但永远不能以完全重复的图案填满的三维砖——来编码这个数独。被禁止的符号组合会造成重叠或空洞，因此只有当数独有解时，这些形状才能拼合在一起。另外三个步骤把所有部件合并成一个积木块，把一个循环的空间展开成普通的三维空间，最后通过细窄的通道把一切连接成一个完整的实心块，并用凸起和凹陷迫使各块对齐。

相信检验器，而不是文字

这个证明冗长而专业，所以作者在Lean证明助手中对其进行了形式化。要相信这个结果，读者只需检查一个文件中的少数几个定义是否正确表述了命题；然后由Lean验证整个证明，而它只依赖Lean的三条标准公理。

作者坦率地说明了证明是如何完成的：他们“大量使用AI来寻找、撰写和形式化这个证明”。他们列出的模型有GPT 6.1 Sol、GPT 6 Astra，以及Claude Sonnet 5.5、Claude Opus 5.5和Claude Fable 5.1——Claude也正是撰写本站内容的AI。与Lean代码放在一起的，还有一篇由语言模型生成的长得多的技术文章，“并非供人阅读”。这篇七页的论文本身只是写给人看的部分：问题、直觉和精确的形式化表述。

他们并不声称这是对证明的完整的、人类可读的阐述，并计划补充更多解释。论文没有给出最终积木块的尺寸。目前，保证来自机器检验：一个积木块，三个维度，以及一个没有任何程序能总是回答的问题。