Preprint
Jul 2026
Lean-Quantum: Toward AI-Assisted Formalization of Quantum Information
This work presents a Lean 4 library for quantum information, designed as a reusable formal infrastructure for theoretical analysis, and formalizes the DPI for the sandwiched R\'enyi relative entropy for positive semidefinite operators on finite-dimensional quantum systems.
Kazumi Kasaura, Kei Tsukamoto, Kento Mori et al.
· 2 citations