Quantum Information
Verifiable foundations for quantum information science
Quantum information theory is the foundation of quantum computing, quantum cryptography, and quantum communication. Proofs in this field weave together results from spectral theory, analysis, and probability in ways that are notoriously difficult to verify by hand. We are building a broad formalization of this field in Lean 4, covering density operators, quantum channels, von Neumann entropy, and cryptographic protocols as reusable verified infrastructure. Our approach is end-to-end rather than piecemeal: we build from eigenvalue perturbation theory and classical entropy through quantum mechanics and information theory, all the way up to security proofs for real protocols like BB84 quantum key distribution.
Why Formalize Quantum Information?
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 does not yet exist in standard proof libraries.
Building in Layers
Mathematical Foundations
Weyl and Ky Fan eigenvalue inequalities, classical Shannon entropy, concentration bounds.
Quantum Mechanics
Density operators, CPTP channels, partial traces.
Information Theory
Von Neumann entropy, Fannes inequality, Fuchs-van de Graaf inequality.
Protocol Security
BB84 key distribution, CSS error-correcting codes.
Key Sorry-Free Results
35,500+ lines of formalized mathematics spanning spectral theory through protocol security.