A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL

TL;DR

This paper formalizes key concepts and results in Quantum Information theory within Isabelle/HOL, including the CHSH inequality and Tsirelson's bound, demonstrating the impossibility of local hidden-variable models.

Contribution

It provides a formal proof of the CHSH inequality and Tsirelson's bound in Isabelle/HOL, advancing the rigor of quantum foundations formalization.

Findings

Formal proof that local hidden-variable hypothesis cannot hold

Formalization of CHSH inequality and its violation

Derivation of Tsirelson's bound for maximum quantum violation

Abstract

We present a formalization of several fundamental notions and results from Quantum Information theory, including density matrices and projective measurements, along with the proof that the local hidden-variable hypothesis advocated by Einstein to model quantum mechanics cannot hold. The proof of the latter result is based on the so-called CHSH inequality, and it is the violation of this inequality that was experimentally evidenced by Aspect who earned the Nobel Prize in 2022 for his work. We also formalize various results related to the violation of the CHSH inequality, such as Tsirelson's bound which permits to obtain the maximum violation of this inequality in a quantum setting.