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 generate certificates that allow verifying our results without trusting either the SAT solver or the CAS. 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倍以上。更重要的是，我们生成验证证书，使得结果可以在无需信任SAT求解器或CAS的情况下得到验证。效率提升源于我们能够利用SAT求解器强大的带有学习能力的组合搜索能力，以及基于CAS的无同构穷举有序图生成方法。据我们所知，我们的工作是SAT+CAS方法在量子基础领域问题中的首次应用，也是最小Kochen-Specker问题中首次获得带有计算机可验证证明证书的下界。