BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//CERN//INDICO//EN
BEGIN:VEVENT
SUMMARY:A Formalization of the Generalized Quantum Stein's Lemma in Lean [
 Confirmed]
DTSTART:20260318T150000Z
DTEND:20260318T163000Z
DTSTAMP:20260419T030900Z
UID:indico-event-2166@events.perimeterinstitute.ca
DESCRIPTION:Speakers: Rodolfo Reis Soldati (Institute for Quantum Computin
 g (IQC))\n\nThe Generalized Quantum Stein's Lemma is a theorem in quantum 
 hypothesis testing that provides an operational meaning to the relative en
 tropy within the context of quantum resource theories. Its original proof 
 was found to have a gap\, which led to a search for a corrected proof. We 
 formalize the proof presented in [Hayashi and Yamasaki (2024)] in the Lean
  interactive theorem prover. This is the most technically demanding theore
 m in physics with a computer-verified proof to date\, building with a vari
 ety of intermediate results from topology\, analysis\, and operator algebr
 a. In the process\, we rectified minor imprecisions in [HY24]'s proof that
  formalization forces us to confront\, and refine a more precise definitio
 n of quantum resource theory. Formalizing this theorem has ensured that ou
 r Lean-QuantumInfo library\, which otherwise has begun to encompass a vari
 ety of topics from quantum information\, includes a robust foundation suit
 able for a larger collaborative program of formalizing quantum theory more
  broadly.\n\nhttps://events.perimeterinstitute.ca/event/2166/
LOCATION:PI/4-405 - Bob Room (Perimeter Institute for Theoretical Physics)
URL:https://events.perimeterinstitute.ca/event/2166/
END:VEVENT
END:VCALENDAR