解法：史密斯–迈尔斯–卡普兰–古德曼-施特劳斯的非周期单块瓷砖:hat 与 Spectre(2023年)
通俗地说
要验证这八条分类规则与匹配检验确实覆盖了 hat 的每一种可能局部排列——没有遗漏,没有歧义,也没有任何排列未被归类——就需要用穷举方式检查数量庞大但有限的小型局部图案。作者们用两个独立的计算机程序完成了这项工作,分别由四位作者中的两位在互不商量的情况下各自编写,并交叉核对确认两者给出相同的结果。
详细分析
由于分类规则以及簇之间的匹配检验必须针对每一种局部可能出现的“ 片”(一块瓷砖连同环绕它的两圈邻居)加以验证,这种情形分析在组合上规模巨大:它要覆盖所有与 hat 的几何结构及此前已建立的匹配规则相容的邻居配置。要手工正确完成而不遗漏任何情形,是不现实的。
因此,Smith, Myers, Kaplan 与 Goodman-Strauss 把情形枚举实现为软件——并吸取了当年四色定理原始证明所引发历史争议的教训——四位作者中的两位在互不合作实现细节的情况下各自独立编写了程序,再比较结果,发现完全一致(2023年,第4节,关于验证的说明)。这种穷举式、经机器检验的情形分析,是论文中第二个主要的计算机辅助步骤(第一个是此前促使这项研究展开的希施数与等边数计算)。
在确认这一分类完整且无歧义之后,现在已知每一个 hat 镶嵌都无一例外地分解为满足所继承匹配规则的四种元瓷砖 ——这为下一步的替换论证铺平了道路。
常见错误. 这一计算机辅助步骤,和四色定理的计算机验证一样,是机械地检查有限但数量极其庞大的情形;作者们应对可靠性担忧的方式,是用两个独立编写的程序进行交叉验证,这是同一思路的一个较轻量版本,后来在其他场合(如四色定理的 Coq 形式化)才被完全实现为机器检验的形式化证明。