Talk at Perimeter Institute: Formally verified quantum information and the Generalized Quantum Stein's Lemma

Created in April 17, 2026

2026   ·   talk,   postdoc,   iqc,   perimeter,   pirsa,   lean,   quantum,   information

I gave a talk at the Quantum Information seminar at Perimeter Institute last month about my work with Alex Meiburg and Léo Lessa on the LEAN programming language.

A Formalization of the Generalized Quantum Stein’s Lemma in Lean

We are building a quantum information theory library for LEAN, and it is now a module of the growing Physlib library that we hope will parallel Mathlib and CSLib! Work towards Physlib includes Joseph Tooby-Smith, and many more. Check it out!



Interested in reading more?

Take a look at these other posts:

  • Quantum Information in L∃∀N!
  • Dedicated to the memory of Ray Laflamme: responsible innovation in quantum technologies
  • QBronze148: O primeiro evento do QBrasil
  • Visit to the Institute for Quantum Computing, Waterloo
  • One person's ancilla is another person's target