Quantum Information
Verified mathematical foundations for quantum information science
Quantum information theory provides the mathematical language for quantum computing, quantum cryptography, and quantum communication. It weaves together spectral theory, operator algebra, entropy, and probability in ways that are both powerful and notoriously difficult to verify by hand. We are building a broad formalization of this field in Lean 4 — not as an end in itself, but as shared, machine-checkable infrastructure that our quantum cryptography and quantum computing projects build upon. The library spans eigenvalue perturbation theory, quantum channels, von Neumann entropy, and information-theoretic bounds, all designed as reusable verified foundations for the science that depends on them.
Infrastructure for Quantum Science
Quantum information proofs combine operator algebra, entropy inequalities, and probabilistic arguments at a level of complexity where errors are easy to introduce and hard to catch. Formalizing these results demands substantial infrastructure — spectral theory, trace norms, CPTP maps, partial traces — that did not previously exist in standard proof libraries. This infrastructure is not only valuable on its own: it is the foundation on which rigorous work in quantum cryptography and quantum computing must rest.
The theorems in this library are significant results in their own right — but they also serve a larger purpose. They are the shared infrastructure on which our Quantum Cryptography and Quantum Computing projects build.
Building in Layers
Spectral Theory
Weyl eigenvalue inequalities, Lieb-Thirring bounds, Ky Fan maximum principle, and Stein three-lines interpolation — the analytical bedrock for entropy and distance arguments throughout quantum information.
Quantum Operators and Channels
Density operators, CPTP maps with full Kraus, Choi-Jamiołkowski, and Stinespring characterization, partial traces, and trace distance contraction — the operator-algebraic infrastructure for quantum mechanics.
Entropy and Information
Von Neumann entropy with full properties and additivity, relative entropy, Klein’s inequality, Fannes continuity bound, and the Holevo bound — the information-theoretic core of quantum science.
Statistical Foundations
Quantum de Finetti theorem with CKMR bounds, Fuchs-van de Graaf inequality, Naimark dilation, data processing inequality, and concentration bounds — the tools that connect theory to protocols.
Verified Theorems
Major results formalized with full machine-checkable proofs in Lean 4.