One of the foundational results in quantum mechanics 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 to exist, the problem of finding the minimum KS vector system has remained stubbornly open for over 55 years, despite significant attempts by leading scientists and mathematicians. In this paper, we present a new method based on a combination of a SAT solver and a computer algebra system (CAS) to address this problem. Our approach shows that a KS system must contain at least 24 vectors and is about 35,000 times more efficient compared to the previous best CAS-based computational methods. Moreover, we generate certificates that provide an independent verification of the results. The increase in efficiency derives from the fact we are able to exploit the powerful combinatorial search-with-learning capabilities of a SAT solver together with the isomorph-free exhaustive generation methods of a CAS. The quest for the minimum KS vector system is motivated by myriad applications such as simplifying experimental tests of contextuality, zero-error classical communication, dimension witnessing, and the security of certain quantum cryptographic protocols. To the best of our knowledge, this is the first application of a novel SAT+CAS system to a problem in the realm of quantum foundations, and the first verified lower bound of the minimum Kochen-Specker problem.

翻译：量子力学的基础成果之一是Kochen-Specker（KS）定理，该定理指出任何预测与量子力学一致的理论必然具有语境性，即量子观测结果无法被理解为揭示预先存在的值。该定理依赖于称为KS向量系统的数学对象的存在性。尽管已知存在许多KS向量系统，但寻找最小KS向量系统的问题在55年多的时间里一直悬而未决，尽管顶尖科学家和数学家为此做出了大量努力。本文提出了一种基于SAT求解器与计算机代数系统（CAS）相结合的新方法来解决此问题。我们的方法表明，一个KS系统必须包含至少24个向量，且效率比此前最优的基于CAS的计算方法高出约35,000倍。此外，我们生成了可独立验证结果的证书。效率的提升源于我们能够利用SAT求解器强大的组合搜索与学习能力，以及CAS的同构排除穷举生成方法。对最小KS向量系统的探索源于多种应用需求，例如简化语境性实验测试、零误差经典通信、维度见证以及某些量子密码协议的安全性验证。据我们所知，这是首次将新型SAT+CAS系统应用于量子基础领域的问题，也是最小Kochen-Specker问题首个经验证的下界结果。