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

arXiv: https://arxiv.org/abs/2510.08672 · HTML: https://mlsanity.com/paper/2510.08672/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 9 Oct 2025.

## Built on by (most cited first, 7 of 7)

- [Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics](https://mlsanity.com/paper/2510.12787/) (2025)
- [MerLean: An Agentic Framework for Autoformalization in Quantum Computation](https://mlsanity.com/paper/2602.16554/) (2026)
- [Formalized Hopfield Networks and Boltzmann Machines](https://mlsanity.com/paper/2512.07766/) (2025)
- [Multi-agent Autoformalization of Tensor Network Theory](https://mlsanity.com/paper/2607.07857/) (2026)
- [Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory](https://mlsanity.com/paper/2607.09632/) (2026)
- [AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics](https://mlsanity.com/paper/2609.05157/) (2026)
- [The Future of AI-assisted Physics: Discovering, Verifying and Organizing Results via Formalization](https://mlsanity.com/paper/2610.14059/) (2026)

## Abstract (arXiv)

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.