QIC 891: Topics in Quantum Information

Quantum Information Theory Modules, Fall 2026

Overview:

Explore formal verification in quantum information theory, and entanglement in infinite-dimensional quantum systems

You can 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.

Attendance:

All IQC and PI members, including students, postdoctoral fellows, and faculty, are welcome to attend the modules without registering if they are not taking the course for credit. Announcements and online discussions will happen on piazza. Please use the following link to sign up.

Coordinator:

Debbie Leung

Announcements:

Modules:

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
Course website:
To be added

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.

Topics:

  • Formal theorem proving in Lean 4
  • Machine-verified mathematics for quantum information theory
  • Core theorem-proving syntax
  • Lean type theory and tactics
  • 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
Course website:
To be added

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.

Topics:

  • Von Neumann algebras as a framework for quantum systems
  • Finite and infinite quantum systems and subsystems
  • Quantum cryptography and entanglement theory in the algebraic framework
  • Operational properties versus structure-theoretic properties
  • Embezzlement of entanglement
  • Operational classification of types I, II, and III von Neumann algebras

Credit:

Students enrolling for credit have to complete one assignment for each module.