解法: スミス=マイヤーズ=カプラン=グッドマン=ストラウスによる非周期単一タイル:ハットとスペクター(2023年)
ざっくり言うと
8つの分類規則と対応確認が、隙間もなく、曖昧さもなく、分類されずに残る配置もない形で、ハットのあらゆる可能な局所配置を本当に網羅していることを確認するには、膨大ではあるが有限個の小さな局所図形を力任せに調べる必要がある。著者らは、4人の著者のうち2人がお互いに相談することなく別々に書いた、二つの独立した計算機プログラムでこれを行い、両方が同じ答えを与えることを相互に確認した。
詳しい解説
分類規則とクラスター間の対応確認は、局所的に可能なあらゆる -パッチ(一つのタイルとそれを取り囲む二重の隣接輪)に対して検証されなければならないため、場合分けは組合せ的に巨大である:これはハットの幾何学とそれまでに確立された対応規則に整合する、許容されるすべての隣接配置を網羅する。これを手作業で、一つも取りこぼすことなく正しく行うのは現実的ではない。
そこでSmith, Myers, Kaplan と Goodman-Strauss は場合の列挙をソフトウェアとして実装し——四色定理の元の証明をめぐる歴史的な論争から学んで——著者のうち二人が実装について協力することなく独立に別々のプログラムを書き、その結果を比較して完全に一致することを確認した(2023年、第4節、検証に関する注記)。この網羅的で機械検証された場合分けは、論文における二番目の主要な計算機支援ステップである(最初のものは、探索の動機となった先のヒーシュ数と等辺数の計算である)。
分類が完全で曖昧さがないことが確認されたことで、ハットによるあらゆるタイル張りは例外なく、継承された対応規則を満たす4種のメタタイル に分解されることが今や分かった——次のステップでの代入の議論への舞台が整った。
よくある間違い. この計算機支援のステップは、四色定理の計算機検証と同様に、有限だが非常に多くの場合を機械的に確認するものである。信頼性への懸念に対する著者らの答えは、別々に書かれた二つのプログラムによる独立した相互検証であり、これは後に他の場面(四色定理のCoq形式化など)で機械検証された形式的証明として完全に実現されることになる、同じ発想の軽量版である。