量子信息理论建立在熵量上，其中夹心R'enyi相对熵是一种具有广泛应用的基本发散量，其在量子通道下的数据处理不等式（DPI）是一个基石结果。在这项工作中，我们提出了一个针对量子信息的Lean 4库，旨在作为理论分析的可重用形式基础。
作为该库的核心示范，我们对有限维量子系统上正半定算子的夹心R'enyi相对熵的DPI进行了形式化。该库提供了一个与标准数学库Mathlib兼容的独立于基的算子理论框架，涵盖有限维系统、态、通道、张量积、部分迹、Choi算子、Kraus表示及Stinespring表示的可重用接口。
此外，它还为非交换迹不等式构建了基础设施，包括通过实连续函数演算实现的算子单调性和凸性、块算子正性、Hilbert-Schmidt算子空间、Jensen算子不等式、广义观点、算子幂均值和Lieb-Ando迹不等式。在此框架之上，我们形式化了DPI的熵特定成分：通过Young和反Young不等式的夹心准熵变分公式、实幂的张量积兼容性以及单位群上的Haar测度。这些组件共同产生了DPI的Lean形式化，强次加性作为推论，并提供了完成广义量子Stein引理的Lean形式化所需的最后一个缺失组件。
更广泛地说，这项开发为未来量子信息理论的形式化和AI辅助研究提供了可机器检查的基础。
博主点评： Lean-Quantum库的推出标志着量子信息理论与形式化验证的结合进入了一个新阶段。通过提供一个强大的框架，研究人员不仅能够更有效地进行理论分析，还能利用AI技术推动量子信息科学的进步。此库的广泛应用潜力值得关注。