Lean-Quantum: Toward AI-Assisted Formalization of Quantum Information

Research Overview

Quantum information theory relies heavily on entropic quantities, with the data processing inequality (DPI) for the sandwiched Rényi relative entropy serving as a cornerstone result. As the field grows in complexity, the need for machine-checkable proofs has become critical to ensure the logical integrity of theoretical developments. This paper introduces a comprehensive Lean 4 library designed to provide a reusable, basis-independent infrastructure for quantum information theory, moving beyond one-off proof encodings.

Approach and Methodology

The authors adopt a coordinate-free approach, representing quantum systems as finite-dimensional Hilbert spaces and operators as linear endomorphisms. This design choice allows the library to leverage existing Mathlib infrastructure, such as the continuous functional calculus and C*-algebraic tools, avoiding the cumbersome dimension bookkeeping associated with matrix-based formalizations. The development follows a modular strategy: first establishing a hierarchy of noncommutative trace inequalities (including Jensen's operator inequality and Lieb-Ando trace inequalities), then formalizing entropy-specific ingredients like variational formulas, and finally proving the DPI for positive definite operators before extending it to the positive semidefinite case.

This work provides a critical bridge between abstract operator theory and practical quantum information research. By formalizing the DPI, the authors fill a significant gap in existing efforts to formalize the generalized quantum Stein's lemma, which previously relied on unverified placeholders. Furthermore, the library's modular design—whereby small, stable interfaces are exposed for local proof search—is specifically optimized for AI-assisted formalization, enabling future researchers to build upon these verified foundations for more complex proofs in quantum hypothesis testing and resource theories.