This repository contains much Lean formalization of quantum information theory. In March 2026, it merged with PhysLean (previously known as HEPLean) and formed Physlib, which is now under the /github.com/leanprover-community umbrella. As such, work on this repository is essentially done, and new development will take place there!
This repository aims to contain definitions and proofs of basic ideas in quantum information theory. Some major goals, in rough order of difficulty, would be:
- Defining most notions of "distance", "entropy", "information", "capacity" that occur in the literature.
- Showing that these reflect the classical notions where applicable
- For instance, that if you embed a clasical probability distribution as a quantum mixed state, then the classical conditional entropy and the quantum conditional entropy are the same number.
- Strong sub-additivity of von Neumann entropy
- Holevo's theorem
- The LSD theorem on quantum capacity
- Non-additivity of quantum capacity
All of this will be done only in the theory finite-dimensional Hilbert spaces. Reasons:
- Most quantum information theory is done in this setting anyway. Not to say that the infinite-dimensional work isn't important, just that this is what more researchers spend their time thinking about.
- Infinite-dimensional quantum theory can be weirdly behaved.
- Dealing with infinite-dimensional quantum theory is just hard. You need e.g. trace-class operators, CTC functions, and people often can't even agree on the definitions. (For instance, does a mixed state necessarily have a finite spectrum? I've seen it both ways.)
Most stuff is in the QuantumInfo/Finite folder. There was a tiny bit of infinite-dimensional theory in the QuantumInfo/InfiniteDim folder, but it's mostly been cleared out.
The docgen is available on my website, hopefully I remember to keep it well synced.
Docmentation of the main definitions can be found at DOC.md. A majority of the work will be outlining the major definitions and theorems from Mark Wilde's Quantum Information Theory. A correspondence to the definitions and theorems (in the form of a todo-list) are in TODO
The initial guiding goal of this repository was completing a proof of the Generalized Quantum Stein's Lemma, following the proof in the linked paper. The first milestone was formalizing all the arguments in that paper (while relying on standard or "obvious" results), which was completed in October 2025. The project was completed when all the other standard results were formalized as well, which was completed in April 2026.
The final theorem is stated as limit_hypotesting_eq_limit_rel_entropy in QuantumInfo/Finite/ResourceTheory/SteinsLemma.lean.
See our report on the project at this link.
As of May 5th 2026 (counts approximate):
- 2143 Theorems
- 423 Definitions
- 38105 Lines of Code
This doesn't include various code snippets that have been upstreamed to Mathlib.
This repository is released under the MIT License, as found in the LICENSE file. Please cite as:
@misc{meiburg2024quantuminfo,
author = {Meiburg, Alex},
title = {Quantum Information in Lean},
year = {2024},
publisher = {GitHub},
journal = {GitHub repository},
howpublished = {\url{https://github.com/Timeroot/Lean-QuantumInfo}},
}
or cite the report for the Stein's Lemma work in particular. Thanks to all contributors, especially Leonardo Lessa and Rodolfo Soldati. Also, thanks to Hayata Yamasaki who has contributed substantial code on operator inequalities (ported to this repository from his own).