One of the fundamental results in quantum foundations is the Kochen-Specker (KS) theorem, which states that any theory whose predictions agree with quantum mechanics must be contextual, i.e., a quantum observation cannot be understood as revealing a pre-existing value. The theorem hinges on the existence of a mathematical object called a KS vector system. While many KS vector systems are known, the problem of finding the minimum KS vector system in three dimensions has remained stubbornly open for over 55 years. In this paper, we present a new method based on a combination of a Boolean satisfiability (SAT) solver and a computer algebra system (CAS) to address this problem. Our approach shows that a KS system in three dimensions must contain at least 24 vectors. Our SAT+CAS method is over 35,000 times faster at deriving the previously known lower bound of 22 vectors than the prior CAS-based searches. More importantly, we provide the first computer-verifiable proof certificate of a lower bound in the KS problem with a proof size of 41.6 TiB in order 23. The increase in efficiency is due to the fact we are able to exploit the powerful combinatorial search-with-learning capabilities of SAT solvers, together with the CAS-based isomorph-free exhaustive method of orderly generation of graphs. To the best of our knowledge, our work is the first application of a SAT+CAS method to a problem in the realm of quantum foundations and the first lower bound in the minimum Kochen-Specker problem with a computer-verifiable proof certificate.

翻译：量子力学基础的核心成果之一是Kochen-Specker（KS）定理，该定理指出，任何预测与量子力学一致的理论都必须是情境性的，即量子观测结果无法被理解为揭示预先存在的值。该定理依赖于一种称为KS向量系统的数学对象的存在性。尽管已有许多KS向量系统被发现，但三维空间中最小KS向量系统的求解问题在过去55年间始终未能解决。本文提出了一种结合布尔可满足性（SAT）求解器与计算机代数系统（CAS）的新方法来解决该问题。我们的方法表明，三维空间中的KS系统必须包含至少24个向量。与先前基于CAS的搜索相比，我们的SAT+CAS方法在推导已知下界（22个向量）时的效率提升了超过35,000倍。更重要的是，我们首次提供了KS问题下界的计算机可验证证明证书——在23阶下，该证明规模达41.6 TiB。效率提升源于我们能够利用SAT求解器强大的组合搜索与学习能力，同时结合基于CAS的无同构穷举图生成方法。据我们所知，本研究是首次将SAT+CAS方法应用于量子力学基础领域，也是首个为最小Kochen-Specker问题下界提供计算机可验证证明证书的工作。