Explore formal verification in quantum information theory, and entanglement in infinite-dimensional quantum systems this fall at IQC.
Develop your understanding of modern quantum information through two focused modules. Attend individual modules based on your interests, or complete both as part of QIC 891 – Topics in Quantum Information for 0.25 course credit.
The first module introduces formal theorem proving with the Lean 4 programming language, providing hands-on experience with machine-verified mathematics and its applications to quantum information theory. The second module examines entanglement in quantum systems described by von Neumann algebras, exploring the mathematical foundations of infinite-dimensional quantum systems and their connections to quantum cryptography and entanglement theory.
All IQC members (students, postdoctoral fellows, and faculty) are welcome to attend the modules without registering if they are not taking the course for credit.
Course Coordinator: Debbie Leung
Piazza sign-up
Course website
Module one: Lean-verified Quantum Information Theory
Instructor: Rodolfo Reis Soldati
Date: September 15, 2026 – October 1, 2026
Time: 10:30am-11:50am
Location: Perimeter Institute
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.
Module two: Entanglement theory for quantum systems described by von Neumann algebras
Instructor: Lauritz van Luijk
Date: October 6, 2026 – October 29, 2026
Time: 10:30am-11:50am
Location: Perimeter Institute
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.