斯滕福多面体嵌入性：基于符号计算的证明

一个多面体若能连续变形且保持其每个面形状和尺寸不变，则称为柔性多面体。20 世纪70年代，Klaus Steffen 构造了一个具有三角形面且仅有 9 个顶点的球面同胚嵌入式柔性多面体，这在柔性多面体理论中广为人知。与此同时，曾提出一种假设，即 Steffen 多面体是所有无边界嵌入式柔性多面体中顶点数最少的。2024 年，Matteo Gallet、Georg Grasegger、Jan Legerský 和 Josef Schicho 构建了一个反驳这一假设的反例。令人惊讶的是，迄今为止尚未在数学文献中发布 Steffen 多面体是否嵌入的证明。可能是因为大家制作这个多面体的纸板模型时都认为这一事实是显而易见的。在本文中，我们使用计算机符号计算证明了这一事实。