Quantum Physics

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.

Although there are good reasons to believe that quantum states are sometimes relativized to observers, there are difficulties for the view that quantum states can only be relativized to conscious macroscopic observers, and also for the view that quantum states can be relativized to any physical system. In this talk, I will argue for an alternative `emergence' approach such that we can indeed write down a description relative to any physical system, but the full formalism of quantum theory emerges only in the limit as the reference system becomes large. If this is true, it poses a challenge for attempts to understand the emergence of the classical regime from the quantum world, since our standard quantum descriptions may presuppose a classical system to which they are relativized. I will describe how this idea might give new insight into Extended Wigner's Friend paradoxes and the measurement problem, and then sketch some ideas for how we might generalize beyond quantum mechanics to characterize descriptions relative to other kinds of reference systems.