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 (3D) has remained stubbornly open for over 55 years. To address the minimum KS problem, we present a new verifiable proof-producing method based on a combination of a Boolean satisfiability (SAT) solver and a computer algebra system (CAS) that uses an isomorph-free orderly generation technique that is very effective in pruning away large parts of the search space. Our method shows that a KS system in 3D must contain at least 24 vectors. We show that our sequential and parallel Cube-and-Conquer (CnC) SAT+CAS methods are significantly faster than SAT-only, CAS-only, and a prior CAS-based method of Uijlen and Westerbaan. Further, while our parallel pipeline is somewhat slower than the parallel CnC version of the recently introduced Satisfiability Modulo Theories (SMS) method, this is in part due to the overhead of proof generation. Finally, we provide the first computer-verifiable proof certificate of a lower bound to the KS problem with a size of 42.9 TiB in order 23.

翻译：量子基础的核心成果之一是Kochen-Specker（KS）定理，该定理指出，任何预测与量子力学一致的理論都必须具有上下文相关性，即量子观测无法被理解为揭示预先存在的值。该定理依赖于一种称为KS矢量系统的数学对象的存在。尽管已知许多KS矢量系统，但在三维（3D）中寻找最小KS矢量系统的问题已顽固未解超过55年。为应对最小KS问题，我们提出了一种新的可验证证明生成方法，该方法结合了布尔可满足性（SAT）求解器和计算机代数系统（CAS），并采用同构免有序生成技术，这种技术在剪枝搜索空间的大片区域方面非常有效。我们的方法表明，3D中的KS系统必须包含至少24个矢量。我们展示了顺序和并行的Cube-and-Conquer（CnC）SAT+CAS方法比仅用SAT、仅用CAS以及Uijlen和Westerbaan先前基于CAS的方法快得多。此外，虽然我们的并行流水线比最近引入的可满足性模理论（SMS）方法的并行CnC版本稍慢，但这部分是由于证明生成的开销。最后，我们首次为KS问题的下界提供了计算机可验证的证明证书，其大小为42.9 TiB，阶数为23。