2025/10/09 by Alex Meiburg, Leonardo A. Lessa, Meiburg, Alex +3 · 2 voices · 4 citations
Physics and Astronomy · Computer Science · #Quantum Mechanics and Applications #Quantum Computing Algorithms and Architecture #Quantum Information and Cryptography
paper · pdf · doi:10.48550/arxiv.2510.08672
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.