Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2510.08672 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914085503762432 |
|---|---|
| author | Meiburg, Alex Lessa, Leonardo A. Soldati, Rodolfo R. |
| author_facet | Meiburg, Alex Lessa, Leonardo A. Soldati, Rodolfo R. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_08672 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Formalization of the Generalized Quantum Stein's Lemma in Lean Meiburg, Alex Lessa, Leonardo A. Soldati, Rodolfo R. Quantum Physics Logic in Computer Science 81P45 (Primary) 62M07, 68V20 (Secondary) F.4.1; H.1.1 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. |
| title | A Formalization of the Generalized Quantum Stein's Lemma in Lean |
| topic | Quantum Physics Logic in Computer Science 81P45 (Primary) 62M07, 68V20 (Secondary) F.4.1; H.1.1 |
| url | https://arxiv.org/abs/2510.08672 |