PIRSA:26030069

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

Reis Soldati, R. (2026). A Formalization of the Generalized Quantum Stein's Lemma in Lean. Perimeter Institute. https://pirsa.org/26030069

Reis Soldati, Rodolfo. A Formalization of the Generalized Quantum Stein's Lemma in Lean. Perimeter Institute, Mar. 18, 2026, https://pirsa.org/26030069 

          @misc{ pirsa_PIRSA:26030069,
            doi = {10.48660/26030069},
            url = {https://pirsa.org/26030069},
            author = {Reis Soldati, Rodolfo},
            keywords = {Quantum Information},
            language = {en},
            title = {A Formalization of the Generalized Quantum Stein{\textquoteright}s Lemma in Lean},
            publisher = {Perimeter Institute},
            year = {2026},
            month = {mar},
            note = {PIRSA:26030069 see, \url{https://pirsa.org}}
          }

Rodolfo Reis Soldati Institute for Quantum Computing (IQC)

Talk numberPIRSA:26030069
DOI10.48660/26030069
Collection
Talk Type Scientific Series
Subject

Abstract

The Generalized Quantum Stein's Lemma is a theorem in quantum hypothesis testing that provides an operational meaning to the relative entropy 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 theorem in physics with a computer-verified proof to date, building with a variety of intermediate results from topology, analysis, and operator algebra. In the process, we rectified minor imprecisions in [HY24]'s proof that formalization forces us to confront, and refine a more precise definition of quantum resource theory. Formalizing this theorem has ensured that our Lean-QuantumInfo library, which otherwise has begun to encompass a variety of topics from quantum information, includes a robust foundation suitable for a larger collaborative program of formalizing quantum theory more broadly.