Lean-verified Quantum Information Theory, Sep 15 - Oct 1 Instructor: Rodolfo Reis Soldati
We introduce formal theorem proving with the Lean 4 programming language, placing emphasis on developing Quantum Information Theory theorems and proofs. Formal proof writing is an increasingly important skill as Quantum Information grows more sophisticated, and as machine-verification tools gain popularity. Participants will learn core theorem-proving syntax, the basics of Lean’s own type theory, the notion and use of tactics, and will gain familiarity with the Mathlib and Physlib/QuantumInfo libraries.
Entanglement theory for quantum systems described by von Neumann algebras, Oct 6 - 29 Instructor: Lauritz van Luijk
In quantum systems with infinitely many degrees of freedom, pairs of subsystems can be infinitely entangled. But are there operationally distinct forms of infinite entanglement? This short course gives a basic mathematical introduction to von Neumann algebras and explains why, when, and how they can be used to describe finite and infinite quantum systems and their subsystems. We will formulate quantum information-theoretic properties, including examples from cryptography and entanglement theory, in this algebraic framework. We will then discuss how some of these operational properties are equivalent to structure-theoretic properties of the von Neumann algebras describing the subsystems. In particular, we answer the opening question by identifying entanglement properties, such as embezzlement of entanglement, that distinguish setups with non-isomorphic algebras. We will see how the classification of von Neumann algebras into types I, II, and III, together with their respective subtypes, can be formulated solely in terms of operational entanglement properties.
Location & Building Access: Please refer to each lecture listing on this site for class location as it will vary from week to week. Perimeter Institute, 31 Caroline St N, Waterloo Participants who do not have an access card for Perimeter Institute must sign in at the security desk before each session. For information on parking or accessibility please contact [email protected].
-
Lecture - Lean-verified Quantum Information Theory, QIC 891
Rodolfo Reis Soldati - Institute for Quantum Computing (IQC)
-
Lecture - Lean-verified Quantum Information Theory, QIC 891
Rodolfo Reis Soldati - Institute for Quantum Computing (IQC)
-
Lecture - Lean-verified Quantum Information Theory, QIC 891
Rodolfo Reis Soldati - Institute for Quantum Computing (IQC)
-
Lecture - Lean-verified Quantum Information Theory, QIC 891
Rodolfo Reis Soldati - Institute for Quantum Computing (IQC)
-
Lecture - Lean-verified Quantum Information Theory, QIC 891
Rodolfo Reis Soldati - Institute for Quantum Computing (IQC)
-
Lecture - Lean-verified Quantum Information Theory, QIC 891
Rodolfo Reis Soldati - Institute for Quantum Computing (IQC)
-
Lecture - Entanglement theory for quantum systems described by von Neumann algebras, QIC 891
Lauritz van Luijk - Leibniz University Hannover
-
Lecture - Entanglement theory for quantum systems described by von Neumann algebras, QIC 891
Lauritz van Luijk - Leibniz University Hannover