Quantum projective measurements and the CHSH inequality in Isabelle/HOL
Mnacho Echenim, Mehdi Mhalla
TL;DR
This paper formalizes quantum projective measurements and the CHSH inequality in Isabelle/HOL, providing a rigorous foundation for quantum measurement theory and Bell inequalities within a proof assistant.
Contribution
It introduces a formalization of quantum projective measurements and the CHSH inequality in Isabelle/HOL, enabling formal reasoning about quantum mechanics and nonlocality.
Findings
Formalization of quantum projective measurements in Isabelle/HOL
Formal proof of the CHSH inequality within the proof assistant
Foundation for automated reasoning in quantum information theory
Abstract
We present a formalization in Isabelle/HOL of quantum projective measurements, a class of measurements involving orthogonal projectors that is frequently used in quantum computing. We also formalize the CHSH inequality, a result that holds on arbitrary probability spaces, which can used to disprove the existence of a local hidden-variable theory for quantum mechanics.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsQuantum Mechanics and Applications · Quantum Information and Cryptography · Philosophy and Theoretical Science