teaching

Lean-verified Quantum Information Theory

• Lean-verified Quantum Information Theory
• Course description and materials
  • Studying materials
  • Project suggestions

A 2026 Fall Term module of QIC891 Topics in Quantum Information

• Class times: Tuesday and Thursday, 10:30am – 11:50am.
• Term dates: from the 15th of September to the 1st of October, 2026.
• Location: Perimeter Institute, room to be determined.
• Github repository: coming soon.
• Lecture recordings: PIRSA (coming soon).

Please see course logistics and administrative information (Piazza, Crowdmark, etc.) on the parent course page by coordinator Prof. Debbie Leung. Every background is welcomed to join, including non-QI researchers.

Our module will be followed by a module on quantum information with von Neumann algebras, taught by Lauritz van Luijk, which I highly recommend checking out. See the page for module 2 Entanglement theory for quantum systems described by von Neumann algebras.

Course description and materials

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

Studying materials

🪏 coming soon

Project suggestions

🪏 coming soon