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 improves the lower bound on the minimum number of vectors in a KS system from 22 to 24, and is about 35,000 times more efficient compared to the previous best computational methods. 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.

翻译：量子力学的基本成果之一是Kochen-Specker（KS）定理，该定理指出，任何预测与量子力学一致的理论都必须是情境相关的，即量子观测不能理解为揭示预先存在的值。该定理依赖于一个数学对象的存在性，称为KS向量系统。尽管已知存在许多KS向量系统，但寻找最小KS向量系统的问题在超过55年的时间里一直悬而未决，尽管顶尖科学家和数学家为此付出了重大努力。本文提出了一种基于SAT求解器与计算机代数系统（CAS）相结合的新方法来解决这一问题。我们的方法将KS系统中最小向量数的下界从22提高到24，并且与先前最佳计算方法相比，效率提升约35000倍。效率的提升源于我们能够利用SAT求解器强大的带学习功能的组合搜索能力，以及CAS的无同构穷举生成方法。寻找最小KS向量系统的动力来自众多应用，例如简化情境性实验测试、零误差经典通信、维度见证以及某些量子密码协议的安全性。据我们所知，这是新型SAT+CAS系统首次应用于量子基础领域的问题。