A Formalization of the CHSH Inequality and Tsirelson’s Upper-bound in Isabelle/HOL | Journal of Automated Reasoning Skip to main content

Advertisement

Springer Nature Link
Log in

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

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

Abstract

We present a formalization of several fundamental notions and results from Quantum Information theory in the proof assistant Isabelle/HOL, 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 quantifies the amount to which this inequality can be violated in a quantum setting.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

Notes

  1. Since then, it has been proven that this phenomenon is in no contradiction with the theory of relativity and does not imply faster-than-light communication.

  2. The superscript is omitted when there is no confusion.

  3. Lemma .

  4. As mentioned in [33], it would be more precise to write in a causally disconnected manner meaning that no information can be transmitted between Alice and Bob. This is ensured in practice by physically separating them, assuming that information cannot travel faster than light.

  5. Including in the original paper on the CHSH inequality [15].

  6. Note that these notions are formalized in a general setting that makes no mention of bipartite states or tensor products.

References

  1. Aspect, A.: Experimental tests of Bell’s inequalities in atomic physics. In: Lindgren, I., Rosén, A., Svanberg, S. (eds.) Atomic Physics 8, pp. 103–128. Springer, Boston (1983)

    Chapter  Google Scholar 

  2. Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52(2), 123–153 (2014)

    Article  MathSciNet  Google Scholar 

  3. Bell, J.S.: On the Einstein Podolsky Rosen paradox. Physics 1(3), 195–200 (1964)

    Article  MathSciNet  Google Scholar 

  4. Berta, M., Brandão, F.G., Gour, G., Lami, L., Plenio, M.B., Regula, B., Tomamichel, M.: On a gap in the proof of the generalised quantum Stein’s lemma and its consequences for the reversibility of quantum resources. arXiv preprint arXiv:2205.02813 (2022)

  5. Boender, J., Kammüller, F., Nagarajan, R.: Formalization of quantum protocols using Coq. Electron. Proc. Theoret. Comput. Sci. 195, 71–83 (2015)

    Article  MathSciNet  Google Scholar 

  6. Bordg, A., Lachnitt, H., He, Y.: Isabelle marries Dirac: a library for quantum computation and quantum information. Archive of Formal Proofs (2020). https://isa-afp.org/entries/Isabelle_Marries_Dirac.html, Formal proof development

  7. Bordg, A., Lachnitt, H., He, Y.: Certified quantum computation in Isabelle/HOL. J. Autom. Reason. 65(5), 691–709 (2021)

    Article  MathSciNet  PubMed  Google Scholar 

  8. Bordg, A., Paulson, L.C., Li, W.: Simple type theory is not too simple: Grothendieck’s schemes without dependent types. Exp. Math. 31(2), 364–382 (2022)

    Article  MathSciNet  Google Scholar 

  9. Brandao, F.G., Gour, G.: Reversible framework for quantum resource theories. Phys. Rev. Lett. 115(7), 070503 (2015)

    Article  ADS  MathSciNet  PubMed  Google Scholar 

  10. Brandao, F.G., Plenio, M.B.: Entanglement theory and the second law of thermodynamics. Nat. Phys. 4(11), 873–877 (2008)

    Article  CAS  Google Scholar 

  11. Brandao, F.G., Plenio, M.B.: A generalization of quantum Stein’s lemma. Commun. Math. Phys. 295, 791–828 (2010)

    Article  ADS  MathSciNet  Google Scholar 

  12. Brandao, F.G., Plenio, M.B.: A reversible theory of entanglement and its relation to the second law. Commun. Math. Phys. 295, 829–851 (2010)

    Article  ADS  MathSciNet  Google Scholar 

  13. Chareton, C., Bardin, S., Bobot, F., Perrelle, V., Valiron, B.: An automated deductive verification framework for circuit-building quantum programs. In: Yoshida, N. (ed.) Programming Languages and Systems—30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27–April 1, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12648, pp. 148–177. Springer, Luxembourg (2021)

  14. Cirel’son, B.S.: Quantum generalizations of Bell’s inequality. Lett. Math. Phys. 4(2), 93–100 (1980)

    Article  ADS  MathSciNet  Google Scholar 

  15. Clauser, J.F., Horne, M.A., Shimony, A., Holt, R.A.: Proposed experiment to test local hidden-variable theories. Phys. Rev. Lett. 23(15), 880–884 (1969)

    Article  ADS  Google Scholar 

  16. Dalton, B.J., Garraway, B.M., Reid, M.D.: Tests for Einstein-Podolsky-Rosen steering in two-mode systems of identical massive bosons. Phys. Rev. A 101, 012117 (2020)

    Article  ADS  CAS  Google Scholar 

  17. Durrett, R.: Probability? Theory and Examples. The Wadsworth & Brooks/Cole Statistics/Probability Series. Wadsworth Inc. Duxbury Press, Belmont (1991)

    Google Scholar 

  18. Echenim, M., Mhalla, M., Mori, C.: The CHSH inequality: Tsirelson’s upper-bound and other results. Archive of Formal Proofs (2023). https://isa-afp.org/entries/TsirelsonBound.html, Formal proof development

  19. Echenim, M.: Quantum projective measurements and the CHSH inequality. Archive of Formal Proofs (2021). https://isa-afp.org/entries/Projective_Measurements.html, Formal proof development

  20. Echenim, M.: Simultaneous diagonalization of pairwise commuting Hermitian matrices. Archive of Formal Proofs (2022). https://isa-afp.org/entries/Commuting_Hermitian.html, Formal proof development

  21. Einstein, A., Podolsky, B., Rosen, N.: Can quantum-mechanical description of physical reality be considered complete? Phys. Rev. 47(10), 777–780 (1935). https://doi.org/10.1103/PhysRev.47.777

    Article  ADS  CAS  Google Scholar 

  22. Fuhrmann, P.A.: Linear systems and operators in Hilbert space. Proc. Edinb. Math. Soc. 26(1), 113–114 (1983). https://doi.org/10.1017/S0013091500028145

    Article  Google Scholar 

  23. Gelfand, I.M., Naimark, M.A.: On the imbedding of normed rings into the ring of operators in Hilbert space. Matematiceskij sbornik 54(2), 197–217 (1943)

    MathSciNet  Google Scholar 

  24. Hensen, B., Bernien, H., Dréau, A.E., Reiserer, A., Kalb, N., Blok, M.S., Ruitenberg, J., Vermeulen, R.F., Schouten, R.N., Abellán, C.: Loophole-free Bell inequality violation using electron spins separated by 1.3 kilometres. Nature 526(7575), 682–686 (2015)

    Article  ADS  CAS  PubMed  Google Scholar 

  25. Hölzl, J.: Construction and stochastic applications of measure spaces in higher-order logic. PhD thesis, Institut für Informatik, Technische Universität München (2012)

  26. Ji, Z., Natarajan, A., Vidick, T., Wright, J., Yuen, H.: MIP*= RE. Commun. ACM 64(11), 131–138 (2021)

    Article  Google Scholar 

  27. Kammüller, F.: Attack trees in Isabelle extended with probabilities for quantum cryptography. Comput. Secur. 87, 101572 (2019)

    Article  Google Scholar 

  28. Kammüller, F., Wenzel, M., Paulson, L.C.: Locales: a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Théry, L., Hirschowitz, A., Paulin, C. (eds.) Theorem Proving in Higher Order Logics, pp. 149–165. Springer, Berlin (1999)

    Chapter  Google Scholar 

  29. Kuncar, O., Popescu, A.: From types to sets by local type definition in higher-order logic. J. Autom. Reason. 62(2), 237–260 (2019)

    Article  MathSciNet  Google Scholar 

  30. Liu, J., Zhan, B., Wang, S., Ying, S., Liu, T., Li, Y., Ying, M., Zhan, N.: Quantum Hoare logic. Archive of Formal Proofs (2019). https://isa-afp.org/entries/QHLProver.html, Formal proof development

  31. Liu, J., Zhan, B., Wang, S., Ying, S., Liu, T., Li, Y., Ying, M., Zhan, N.: Formal verification of quantum algorithms using Quantum Hoare Logic. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification, pp. 187–207. Springer, New York (2019)

    Chapter  Google Scholar 

  32. Mermin, N.D.: Hidden variables and the two theorems of John Bell. Rev. Mod. Phys. 65, 803–815 (1993)

    Article  ADS  MathSciNet  Google Scholar 

  33. Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information: 10th Anniversary Edition, 10th edn. Cambridge University Press, Cambridge (2011)

    Google Scholar 

  34. Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle/HOL. Springer, New York (2014)

    Book  Google Scholar 

  35. Rand, R., Paykin, J., Zdancewic, S.: Qwire practice: formal verification of quantum circuits in Coq. Electron. Proc. Theoret. Comput. Sci. 266, 119–132 (2018). https://doi.org/10.4204/EPTCS.266.8

    Article  Google Scholar 

  36. Ruan, M.Q., Zeng, J.Y.: Complete sets of commuting observables of Greenberger-Horne-Zeilinger states. Phys. Rev. A 70, 052113 (2004). https://doi.org/10.1103/PhysRevA.70.052113

    Article  ADS  CAS  Google Scholar 

  37. Scarani, V.: Bell Nonlocality. Oxford Graduate Texts. Oxford University Press, Oxford (2019)

    Book  Google Scholar 

  38. Scherer, W.: Mathematics of Quantum Computing: An Introduction. Springer, Switzerland (2019). https://doi.org/10.1007/978-3-030-12358-1

    Book  Google Scholar 

  39. Storz, S., Schär, J., Kulikov, A., Magnard, P., Kurpiers, P., Lütolf, J., Walter, T., Copetudo, A., Reuer, K., Akin, A.: Loophole-free Bell inequality violation with superconducting circuits. Nature 617, 265–270 (2023)

    Article  ADS  CAS  PubMed  PubMed Central  Google Scholar 

  40. Thiemann, R., Yamada, A.: Formalizing Jordan normal forms in Isabelle/HOL. In: Avigad, J., Chlipala, A. (eds.) Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20–22, 2016, pp. 88–99. ACM, USA (2016)

  41. Thiemann, R., Yamada, A.: Matrices, Jordan normal forms, and spectral radius theory. Archive of Formal Proofs (2015). https://isa-afp.org/entries/Jordan_Normal_Form.html, Formal proof development

  42. Unruh, D.: Quantum relational Hoare logic. Proc. ACM Programm. Lang. 3, 1–31 (2019). https://doi.org/10.1145/3290346

    Article  Google Scholar 

  43. Vidick, T.: Three-player entangled XOR games are NP-hard to approximate. SIAM J. Comput. 45(3), 1007–1063 (2016)

    Article  MathSciNet  Google Scholar 

Download references

Acknowledgements

This work benefited from the funding program “Plan France 2030” (ANR-22-PETQ-0007) of the French National Research Agency.

Author information

Authors and Affiliations

  1. Université Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes), LIG, 700 avenue Centrale, 38400, Saint Martin d’Hères, France

    Mnacho Echenim & Mehdi Mhalla

Authors
  1. Mnacho Echenim
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mehdi Mhalla
    View author publications

    You can also search for this author in PubMed Google Scholar

Contributions

ME and MM wrote the main manuscript text and they both reviewed the manuscript.

Corresponding authors

Correspondence to Mnacho Echenim or Mehdi Mhalla.

Ethics declarations

Competing interests

The authors declare no competing interests.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Echenim, M., Mhalla, M. A Formalization of the CHSH Inequality and Tsirelson’s Upper-bound in Isabelle/HOL. J Autom Reasoning 68, 2 (2024). https://doi.org/10.1007/s10817-023-09689-9

Download citation

  • Received:

  • Accepted:

  • Published:

  • DOI: https://doi.org/10.1007/s10817-023-09689-9

Keywords

Search

Navigation