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问题中首个附带计算机可验证证明证书的下界结果。