量子科技中心_量科网

对克劳瑟-霍恩-西莫尼-霍尔特（CHSH）不等式的违背验证了真正的量子关联性。该工作采用Lean 4形式化系统证明了刚性定理——任何达到接近最优CHSH值的策略，在局部上必然与标准量子比特策略等距同构。在形式化过程中，研究人员发现McKague、Yang和Scarani（arXiv:1203.2976）的论证存在漏洞。