Quantum Wednesday: Formalizing Quantum Information in Lean

Wednesday, October 22, 12:30pm - 1:30pm (EDT)

Time shown in-05:00 America, New York

Come join the Unitary Foundation team for Quantum Wednesday! Here we review recent papers, discuss research questions, and invite speakers on interesting topics related to quantum software and error mitigation.

Talk type: Invited speaker
Speaker: Alex Meiburg
Paper URL (if provided): https://github.com/Timeroot/Lean-QuantumInfo
Abstract (if provided):
We've formalized the Generalized Quantum Stein's Lemma in Lean, a theorem about resource theories that was at one point cast into doubt when a major error was found in the twelve-year-old proof. In the process we've built up a large repository of QI concepts in the Lean theorem prover.

Add to Calendar 2025/10/22 09:30:00 2025/10/22 10:30:00 America/Los_Angeles Quantum Wednesday: Formalizing Quantum Information in Lean Come join the Unitary Foundation team for Quantum Wednesday! Here we review recent papers, discuss research questions, and invite speakers on interesting topics related to quantum software and error mitigation.

Talk type: Invited speaker
Speaker: Alex Meiburg
Paper URL (if provided): https://github.com/Timeroot/Lean-QuantumInfo
Abstract (if provided):
We've formalized the Generalized Quantum Stein's Lemma in Lean, a theorem about resource theories that was at one point cast into doubt when a major error was found in the twelve-year-old proof. In the process we've built up a large repository of QI concepts in the Lean theorem prover. #community-call channel on http://discord.unitary.foundation false MM/DD/YYYY OPAQUE alhPbYnQkzqmdznZemwC129713

#community-call channel on http://discord.unitary.foundation

Link: