A Formalization of the CHSH Inequality and Tsirelson's Upper-bound in Isabelle/HOL

Mnacho Echenim, Mehdi Mhalla. A Formalization of the CHSH Inequality and Tsirelson's Upper-bound in Isabelle/HOL. Journal of Automated Reasoning, 68(1):2, March 2024. [doi]

Abstract

Abstract is missing.