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

• URL: http://arxiv.org/abs/2510.08672v1
• Date: Thu, 09 Oct 2025 17:41:13 GMT
• Title: A Formalization of the Generalized Quantum Stein's Lemma in Lean
• Authors: Alex Meiburg, Leonardo A. Lessa, Rodolfo R. Soldati,
• Abstract summary: We formalize the proof presented inHayashi and Yamasaki (2024) in the Lean interactive theorem prover.<n>This is the most technically demanding theorem in physics with a computer-verified proof to date.
• Score: 0.0
• License: http://creativecommons.org/licenses/by-sa/4.0/
• 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.

Related papers

• Majorization theory for quasiprobabilities [0.49478969093606673]
  Majorization theory is a powerful tool to compare the disorder in distributions.<n>We introduce a notion of majorization for continuous quasiprobability distributions over infinite measure spaces.<n>We give several applications of our results in the context of quantum resource theories.
  arXiv  Detail & Related papers  (2025-07-30T18:00:03Z)
• Some mathematical issues regarding a new approach towards quantum foundations [0.0]
  The weakest possible theorem providing a foundation for the Hilbert space formalism of quantum theory is stated.<n>Some applications to the Bell experiment and to decision theory are briefly discussed.
  arXiv  Detail & Related papers  (2024-11-20T08:14:14Z)
• Generalized Quantum Stein's Lemma and Second Law of Quantum Resource Theories [47.02222405817297]
  A fundamental question in quantum information theory is whether an analogous second law can be formulated to characterize the convertibility of resources for quantum information processing by a single function.<n>In 2008, a promising formulation was proposed, linking resource convertibility to the optimal performance of a variant of the quantum version of hypothesis testing.<n>In 2023, a logical gap was found in the original proof of this lemma, casting doubt on the possibility of such a formulation of the second law.
  arXiv  Detail & Related papers  (2024-08-05T18:00:00Z)
• Generalized Quantum Stein's Lemma: Redeeming Second Law of Resource Theories [1.90365714903665]
  This note is a temporal update to add this note. We are planning to update the manuscript further to explain the issue and what conditions we will additionally need to complete the proof of the generalized quantum Stein's lemma.
  arXiv  Detail & Related papers  (2024-01-03T19:00:00Z)
• A simple formulation of no-cloning and no-hiding that admits efficient and robust verification [0.0]
  Incompatibility is a feature of quantum theory that sets it apart from classical theory. The no-hiding theorem is another such instance that arises in the context of the black-hole information paradox. We formulate both of these fundamental features of quantum theory in a single form that is amenable to efficient verification.
  arXiv  Detail & Related papers  (2023-03-05T12:48:11Z)
• Advantages of quantum mechanics in the estimation theory [0.0]
  In quantum theory, the situation with operators is different due to its non-commutativity nature. We formulate, with complete generality, the quantum estimation theory for Gaussian states in terms of their first and second moments.
  arXiv  Detail & Related papers  (2022-11-13T18:03:27Z)
• Depth-efficient proofs of quantumness [77.34726150561087]
  A proof of quantumness is a type of challenge-response protocol in which a classical verifier can efficiently certify quantum advantage of an untrusted prover. In this paper, we give two proof of quantumness constructions in which the prover need only perform constant-depth quantum circuits.
  arXiv  Detail & Related papers  (2021-07-05T17:45:41Z)
• Quantum Causal Inference in the Presence of Hidden Common Causes: an Entropic Approach [34.77250498401055]
  We put forth a new theoretical framework for merging quantum information science and causal inference by exploiting entropic principles. We apply our proposed framework to an experimentally relevant scenario of identifying message senders on quantum noisy links. This approach can lay the foundations of identifying originators of malicious activity on future multi-node quantum networks.
  arXiv  Detail & Related papers  (2021-04-24T22:45:50Z)
• Quantum simulation of gauge theory via orbifold lattice [47.28069960496992]
  We propose a new framework for simulating $textU(k)$ Yang-Mills theory on a universal quantum computer. We discuss the application of our constructions to computing static properties and real-time dynamics of Yang-Mills theories.
  arXiv  Detail & Related papers  (2020-11-12T18:49:11Z)
• One-shot quantum error correction of classical and quantum information [10.957528713294874]
  Quantum error correction (QEC) is one of the central concepts in quantum information science. We provide a form of capacity theorem for both classical and quantum information. We show that a demonstration of QEC by short random quantum circuits is feasible.
  arXiv  Detail & Related papers  (2020-11-02T01:24:59Z)
• Using Quantum Metrological Bounds in Quantum Error Correction: A Simple Proof of the Approximate Eastin-Knill Theorem [77.34726150561087]
  We present a proof of the approximate Eastin-Knill theorem, which connects the quality of a quantum error-correcting code with its ability to achieve a universal set of logical gates. Our derivation employs powerful bounds on the quantum Fisher information in generic quantum metrological protocols.
  arXiv  Detail & Related papers  (2020-04-24T17:58:10Z)
• From a quantum theory to a classical one [117.44028458220427]
  We present and discuss a formal approach for describing the quantum to classical crossover. The method was originally introduced by L. Yaffe in 1982 for tackling large-$N$ quantum field theories.
  arXiv  Detail & Related papers  (2020-04-01T09:16:38Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.