数学家找到顶点数最少的 nopert 多面体：七顶点的 Septopert

Septopert 是一个有 7 个顶点的凸多面体，它不是 Rupert 多面体（即“nopert”）。7 个顶点是 nopert 可能的最少顶点数。本页描述的规范 Septopert 是一族相似 nopert 中最好的版本，该家族还包括正模标本 Septopert Classic、SeptopertM18 和 SeptopertM12。它的整数坐标是该家族中 nopert 可能的最小值（见下文“最小高度”）。本页给出精确陈述、Lean 检查了什么以及如何检查、以及如何复现结果。

Lean 入口点：proof/Septopert.lean；主定理位于 proof/Septopert/Integer.lean。

这里有一个精确的 STL 文件。在 github 上，你只需点击它就可以在浏览器中旋转它。

Septopert 是以下点（其顶点）的凸包： (-7, 7, 7) ( 7, -7, 7) ( 7, 7, -7) ( 3, -4, -4) (-4, 3, -4) (-4, -4, 3) ( 7, 7, 7)

它是一个非常“7”的立体：7 个顶点，坐标为 ±7 和 3、4（3 + 4 = 7），顶点棱长为 14，底边长为 14√2，内部三角形边长为 7√2。尽管是由 Tom 7 发现的，这种“七重性”其实只是数学上的巧合！中了头奖！

Lean 陈述针对的正是这些整数点（最大的 |v| = √147 ≈ 12.12）。该立体的任何缩放或刚性变换也都是 Nopert。（在内部，证明实际上复用了某些较旧的机制，并在不同的坐标系和尺度下工作，然后用引理证明上述顶点的陈述。）

精确算术（整数面法向量；长度基于上述整数坐标）。 （注：这是用于 Septopert 家族任意成员的示意图，并非精确图。）

theorem isNopert_intVerts (h : CertificatesValid) : IsNopert intVerts

intVerts 是上述七个整数点的集合（septopert 是它的另一个名字）。

IsNopert、IsRupert 和信任模型与 SeptopertM18 相同。CertificatesValid 表示证书数据（四个解表、镜像帽证书，以及三个特殊帽：弧帽、轴帽和 P 帽）通过了 Lean 的有效性检查。最小性结果使用同一个 IsNopert，而 Septopert 是 proof/ProofOfMainTheorem.lean 中的 7 顶点见证。

证书是在该立体的一个全等副本中构建的（verts，坐标以 64 为分母：(−27,15,15)、(27,6,6)、(−13,−13,−13) 及其排列）。一个简短的桥接引理通过精确相似变换（缩放 3/64、绕轴反射与绕轴 180° 旋转的复合、以及平移）将其映射到整数坐标，而相似变换保持 Rupert 性。

与 SeptopertM18 一样：isNopert_intVerts 由 Lean 内核检查，并且只依赖于标准公理（propext、Classical.choice、Quot.sound）。数据（约 732,000 行表格和帽证书）由程序 constructSeptopert 检查，该程序以编译代码运行相同的 Lean 有效性检查，然后才构造 IsNopert intVerts，并打印 instantiated: IsNopert Septopert.intVerts (CapOk, ArcOk, AxisOk, PCapOk checked natively; tube and chart tables checked)

其他 Septopert

本页描述的是规范 Septopert，它在该家族中具有最小的整数坐标。它（我们认为）位于该家族的边缘，处于一个具有精确立方体角和精确 Triforce 的特殊位置。

我们在过程中还证明了该家族的其他几个成员是 nopert：

所用技术是 How the Nopert proofs work 中的技术，使用 SeptopertM18 的弧帽。视图覆盖有 13 个视图代码和 16 个视图代码三角形（SeptopertM18：15 和 22）。管道和 5D 搜索封闭了除四个小视图区域之外的所有内容，每个区域都需要一个放大证书，因为一阶裕量在那里消失：

在每种情况下，判定都转移到二阶，其中间隙严格为负，这就是证书存在的原因（浮点和符号研究，不属于证明的一部分）。

用五个坐标值 x = (x0, ..., x4) 来写该家族的一个成员：点 (x0, x1, x1)、(x2, x3, x3) 及其排列，以及 (x4, x4, x4)。其高度是这些值范围的一半，向上取整。Septopert 的值为 −7、7、3、−4、7（范围 14），所以其高度为 7。没有更低高度的整数成员是 nopert。在 proof/SeptopertFamily.lean 中：

theorem not_isNopert_of_familyHeight_lt_seven (hvalid : LeastHeightValid) : ∀ x : Fin 5 → ℤ, familyHeight x < 7 → ¬ IsNopert (familyVerts x)

该陈述覆盖每个整数元组，符号任意。平移、缩放和反射元组保持 nopert 性（已在 Lean 中证明），因此它归结为 55,651 个规范元组，值在 [0, 12] 中，每个都有一个由 checkSeptopertFamily 检查的小证书（约 4 秒）：

表格是 proof/SeptopertFamily/data/leastheight.txt（2.7 MB）。与其他结果一样，这是一个内核定理（公理 propext、Classical.choice、Quot.sound）加上对数据的原生检查。

验证于 2026-11-07：constructSeptopert（然后是 constructM7）检查了镜像帽（52 个图表）、弧帽（146 个图表，22,282 个叶节点）、轴帽（52 个图表，3,384 个叶节点）、P 帽（78 个图表，43,869 个叶节点）、管道表，以及四个图表表（406,726、124,781、108,449 和 92,514 行），并打印了上面实例化的行。在一台繁忙机器的 12 个核心上，大约花了 23 分钟（各阶段时间：镜像帽 196 秒，弧帽 723 秒，轴帽 16 秒，P 帽 300 秒，表格为其余时间）。

然后于 2026-11-08 从头复现，从该仓库的全新克隆（提交 3d8fce61）开始，在一台其他方面空闲的 64 核机器上使用 60 个线程。所有阶段，包括三个特殊帽证书，都被重新生成；图表表具有与上面相同的行数，重新生成的模型文件与提交的文件匹配，并且 constructSeptopert 打印了相同的实例化行：

./get-cc-lib.sh (cd proof && lake exe cache get) # Mathlib build cache search/septopert/rebuild.sh --threads 60 --work work-fresh

搜索是多线程且非确定性的，因此其他运行可能

（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）