2025/10/09 by Alex Meiburg, Leonardo A. Lessa, Meiburg, Alex +3 · 2 voices · 4 citations
Computer Science · Physics and Astronomy · #Algebra over a field #Calculus (dental) #Context (archaeology) #Lemma (botany) #Operator (biology) #Quantum #Quantum Computing Algorithms and Architecture #Quantum Information and Cryptography #Quantum Mechanics and Applications #Quantum information #Quantum no-deleting theorem #Variety (cybernetics)
paper · pdf · doi:10.48550/arxiv.2510.08672
published in arXiv (Cornell University) (Cornell University)
openalex publication_date 2025/10/09 · openalex created_date 2025/10/14 · openalex updated_date 2026/08/05
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.