Tom7 发布可复现的 Nopert 形式化证明，完成 P/A/C 多面体分类

这是关于 Noperts 的一系列形式化结果。

如果一个形状能够将自身的精确副本穿过自身，则称该形状为 Rupert 形状。它得名于鲁珀特亲王立方体（Prince Rupert's Cube），这是立方体能够做到这一点的首个著名演示。令人惊讶的是，大多数凸多面体都是 Rupert 的，而且在 2025 年之前，人们甚至不知道是否存在任何反例。我们将不是 Rupert 的多面体称为“Nopert”，即 Nope + Rupert。

你可以在我的 2025 年 SIGBOVIK 论文《Some upsetting things about shapes (that we already knew)》、后来的 YouTube 视频《Rupert's Snub Cube and other Math Holes》中了解更多关于 Rupert 和 Nopert 的内容；如果你想要更严肃的论述，可以看 Wikipedia。

其他地方有声称的证明或验证表明菱形二十面体（rhombicosidodecahedron）[1], [2] 是 Nopert 的，并且我们也有其余柏拉图立体、阿基米德立体和卡塔兰立体的解。所以这终于对全部 P/A/C 立体完成了分类！

Nopert 验证涉及巨大的情况分析。所以当我说“验证”时，我指的是依赖于外部数据文件的证明。我们证明了一个真正的定理（仅依赖 Lean 内核），它大致是说“如果这个 Lean 程序验证了证书，那么该形状不是 Rupert”，然后我们运行程序来确认它确实验证了证书。这意味着需要信任比仅依赖内核的证明更多的东西（类似于使用 native_decide 的证明）；Lean 编译器和运行时也必须正确。证书是由 C++ 代码找到的，这些代码不需要被信任。证书也太大（许多 GB），无法包含在内，所以要复现结果，你需要使用脚本重新构建它们。证明技术描述在《How the Nopert proofs work》中。

这就是 Septopert，按顶点数（七个）最小的 Nopert。

它们在这里： (-940638, 327651, 327651) ( 327651, -940638, 327651) ( 327651, 327651, -940638) ( 703968, 47788, 47788) ( 47788, 703968, 47788) ( 47788, 47788, 703968) (-514207, -514207, -514207)

它具有三重对称性，所以你会一遍又一遍地看到相同的数字。

在证明（proof/Septopert.lean）中，我们将所有东西除以 2^20（1048576），使得该立体的半径接近 1，你可能也想这样做，除非你想要一个非常大的 Nopert。Rupert 性质在缩放和刚性变换下当然是不变的。

这里是 septopert.stl，一个你可以进行 3D 打印的模型。

这项工作大量建立在 Jason Reed、David Renshaw 等人对 Noperthedron 的形式化工作之上。那又是对 Jakob Steininger 和 Sergey Yurkevich 的论文《A convex polyhedron without Rupert's property》（“SY25”）的形式化，该论文引入了 Noperthedron 及其原始验证。

AI：这里涉及的 AI 多到令人尴尬。David 做了证明我的“Candidate 214”（以及其他一些未解决的立体）的初步尝试。这需要扩展数学以处理非点对称立体等。他为此使用了 Sol 5.6 和 Fable 5.0。但他实际上最终发现我的 #214 是 Rupert 的。我从那里接手，目标是修复 #214 以挽回面子。使用 Antigravity（Gemini 3.7 和 3.8 Flash）和 Claude Code（Opus 5.5），我验证了一个修复后的、外观相同的形状 #231。这个证明并不容易，而且确实使用了我最初尝试证明 snub cube（第一个 Nopert）时的想法，但你可以从我在希腊度假时完成了它这一点看出其中有多少实际上是 AI 的功劳！它曾短暂地成为已证明的最小 Nopert，有 20 个顶点和 27 个面。

与此同时，我们了解到今年早些时候，Tony Zeng 提出了一个更小的立体（8 个顶点）作为 Nopert 的候选。David 能够使用改进后的机制在 Lean 中验证它。

这作为已证明的最小 Nopert 只维持了大约一天。我同时在竞相验证一个 7 顶点的形状，即上面描述的 Septopert，这是我用我的对抗性求解器通过计算机搜索找到的。它只是勉强是 Nopert 的，所以证明需要一个大证书（7 GB 的打包数据）。我在 10 月 9 日验证了它，在一台 64 核的巨兽上花了大约 4 小时。

那么自然的问题是：我们能找到一个六顶点的 Nopert 吗？或者也许我们可以证明每个四面体都是 Rupert 的？或者每个五顶点立体？从 Jason 2025 年的一些想法出发，并且我愿意认为还有其学术顾问兼监工（我）的一些明智指导，Opus 5.5 能够在大约一天内证明这一点（仅依赖 Lean 内核的证明）：所有六顶点或更少的凸立体都是 Rupert 的。这意味着 Septopert 是一个最小的 Nopert（按顶点数）。

证书的大小很烦人，因为这意味着你必须重新运行 C++ 代码。在验证这些形状之后，我们对流水线进行了几轮改进，以提高搜索、证书和验证的效率。这目前还不完整，但我希望很快就能直接将证书包含在仓库中，这样你就可以仅使用 Lean 来复现验证。

Lean 代码（proof/）是 Apache 2.0。C++ 代码（search/）是 GPLv3，除非另有说明。