KO | EN

GitLite

Minimalist Open Source Repository Search Engine

gitlite — search

#dsh #dsh-plugin #ai-agent #developer-tools #codex #typescript #cli #deepseek-harness #claude-code #ai-agents #mcp #rust

Lean-QuantumInfo

★ 141 Open GitHub ↗

Quantum information theory in Lean 4

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# NOTE: This project is now part of Physlib

This repository contains much Lean formalization of quantum information theory. In March 2026, it merged with PhysLean (previously known as HEPLean) and
formed [Physlib](https://github.com/leanprover-community/physlib), which is now under the [/github.com/leanprover-community](https://github.com/leanprover-community)
umbrella. As such, work on this repository is essentially done, and new development will take place there!

# Quantum Information in Lean

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](https://en.wikipedia.org/wiki/Quantum_capacity#Hashing_bound_for_Pauli_channels) 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](https://en.wikipedia.org/wiki/Connes_embedding_problem).
* 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](https://ohaithe.re/Lean-QuantumInfo/QuantumInfo.html), hopefully I remember to keep it well synced.

[comment]: # (Note to self, instructions for building docs: `rm -rf .lake/build/doc/QuantumInfo* .lake/build/doc/ClassicalInfo*; lake -R -Kenv=dev build ClassicalInfo:docs QuantumInfo:doc`. In order to view them, `cd .lake/build/doc; python3 -m http.server`.)

Docmentation of the main definitions can be found at [DOC.md](./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](./TODO.md)

# Major Accomplishment: Generalized Quantum Stein's Lemma

The initial guiding goal of this repository was completing a proof of the [Generalized Quantum Stein's Lemma](https://arxiv.org/abs/2408.02722v1), 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](https://arxiv.org/abs/2510.08672).

# Stats

This doesn't include various code snippets that have been upstreamed to Mathlib.

# Attribution

This repository is released under the MIT License, as found in the [LICENSE](./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](https://arxiv.org/abs/2510.08672) 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).

Lean-QuantumInfo

Explore Similar Repositories

Was this content helpful?

Recent Feedback

Download README