Machine-Checked Certificates for the Geometric Half of the Minimum Kochen-Specker Bound
本論文は、公開されているブロッキング・データベース内の180個の異なるすべてのグラフの幾何学的な非埋め込み性を、正確な有理数ケースツリー証明書と2つの独立したチェッカー(一つはPython、もう一つはLean 4で形式的に証明されたもの)を導入することで機械的に検証することにより、最小コヘン・スペッカー境界における決定的な検証の空白を埋め、それによって未検証のZ3による決定をカーネル検証済みの定理へと置き換えると同時に、元の証明パイプラインにおけるいくつかの隠れた欠陥や不一致を明らかにし、解決するものである。