Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Alex Meiburg, Leonardo A. Lessa, Rodolfo R. Soldati

TL;DR

The paper delivers a formal Lean proof of the Generalized Quantum Stein's Lemma (GQSL), addressing gaps identified in prior proofs and embedding the result within a robust Lean-QuantumInfo library built on mathlib. It develops the finite-dimensional quantum infrastructure, carefully handles extended reals and junk values, and formalizes the GQSL statement with corresponding definitions (e.g., $eta_ obrace _ ( ho^{\otimes n} \| \mathcal S_n)$ and $D(\rho^{\otimes n} \| \sigma)$) to relate the exponential rate of type-II error decay to the regularized relative entropy. The work emphasizes end-to-end formal verification of the first half of HY24 up to the GQSL and identifies remaining axioms to be proven (e.g., data processing, continuity properties of entropy, and pinching results). It also outlines future directions to generalize to non-unital quantum resource theories and to derive corollaries such as the Second Law of QRTs, positioning Lean as a practical platform for large-scale formalization of quantum information theory.

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.

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

TL;DR

The paper delivers a formal Lean proof of the Generalized Quantum Stein's Lemma (GQSL), addressing gaps identified in prior proofs and embedding the result within a robust Lean-QuantumInfo library built on mathlib. It develops the finite-dimensional quantum infrastructure, carefully handles extended reals and junk values, and formalizes the GQSL statement with corresponding definitions (e.g., and ) to relate the exponential rate of type-II error decay to the regularized relative entropy. The work emphasizes end-to-end formal verification of the first half of HY24 up to the GQSL and identifies remaining axioms to be proven (e.g., data processing, continuity properties of entropy, and pinching results). It also outlines future directions to generalize to non-unital quantum resource theories and to derive corollaries such as the Second Law of QRTs, positioning Lean as a practical platform for large-scale formalization of quantum information theory.

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.

Paper Structure

This paper contains 20 sections, 1 theorem, 22 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Background
  3. Proof formalization
  4. Example: No-cloning theorem
  5. Generalized quantum Stein's lemma
  6. Outcomes of the Formalization
  7. Imprecisions in the existing proof
  8. Design and Development Choices
  9. Foundations of quantum theory
  10. Definition of quantum resource theory
  11. Numerical convention
  12. Junk values
  13. Behavior of extended nonnegative reals
  14. Other mathematical hurdles
  15. Comparison with other physics formalizations
  16. ...and 5 more sections

Key Result

Theorem 1

For any $\varepsilon\in(0,1)$ and any sequence $\{\mathcal{S}_n\}_n$ of sets of states satisfying Conditions 1, 2, and 3 above, we have

Figures (2)

  • Figure 1: An interacting theorem proving system, such as Lean, is a tool with which the user constructs a proof, and the computer formally verifies it.
  • Figure 2: Lean's InfoView showing the state of the no-cloning proof just after proving proposition , as indicated by the comment in the code listing. All terms from the local scope are explicitly stated along with their definitions, with the current goal ($\vdash \langle\psi, \varphi\rangle = 0$) at the end. As the proof evolves, both the list of hypotheses and the goal can change.

Theorems & Definitions (1)

  • Theorem 1: Generalized quantum Stein's lemma hayashi2024