Projective Measurements and the CHSH inequality with Isabelle/HOL
- Imprimer
- Partager
- Partager sur Facebook
- Share on X
- Partager sur LinkedIn
Mercredi 28 avril 2021
Abstract
Interactive theorem provers are tools that permit users to produce formal mathematical proofs. These tools have been used to guarantee that highly non-trivial proofs are indeed correct, and, in some cases, have permitted the detection of gaps in already published proofs.
In this talk we investigate how interactive theorem provers can be used in the context of quantum computing, by formalizing fundamental notions from this domain. More precisely, we present a formalization of projective measurements in Isabelle/HOL, along with the formal construction of the projective measurement associated with a given observable. We also formalize local joint probability distributions and the CHSH inequality, which permits to prove that there is no local hidden-variable theory for quantum mechanics.
Date et Lieu
Mercredi 28 avril, 14h00
https://univ-grenoble-alpes-fr.zoom.us/j/94612751658?pwd=bHgzVFYra29sYlA5Vlp1MzVuT1pEQT09
Organisé par
Nicolas PELTIER
Chef d'équipe : CAPP
Intervenant
Mnacho ECHENIM
CAPP, candidat à un poste de professeur Ensimag
- Imprimer
- Partager
- Partager sur Facebook
- Share on X
- Partager sur LinkedIn