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

arXiv: https://arxiv.org/abs/2607.05492 · HTML: https://mlsanity.com/paper/2607.05492/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 17 references that are in the map.
- First posted on arXiv 6 Jul 2026.

## Builds on (most cited first, 8 of 8)

- [A Machine Learning Approach to the Nirenberg Problem](https://mlsanity.com/paper/2602.12368/) (2026)
- [Neural and numerical methods for G2-structures on contact Calabi-Yau 7-manifolds](https://mlsanity.com/paper/2602.12438/) (2026)
- [Minimising Willmore Energy via Neural Flow](https://mlsanity.com/paper/2604.04321/) (2026)
- [Machine Learning Gravity Compactifications on Negatively Curved Manifolds](https://mlsanity.com/paper/2501.00093/) (2024)
- [Einstein Fields: A Neural Perspective To Computational General Relativity](https://mlsanity.com/paper/2507.11589/) (2025)
- [Minimal surfaces, Knots, and Neural Networks](https://mlsanity.com/paper/2605.26234/) (2026)
- [Machine learning automorphic forms for black holes](https://mlsanity.com/paper/2505.05549/) (2025)
- [PINNs in More General Geometry](https://mlsanity.com/paper/2604.25020/) (2026)

## Built on by (most cited first, 1 of 1)

- [AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics](https://mlsanity.com/paper/2609.05157/) (2026)

## Abstract (arXiv)

Quantum information theory is built on entropic quantities; among them, the sandwiched R'enyi relative entropy is a fundamental divergence with various applications, and its data processing inequality (DPI) under quantum channels is a cornerstone result. In this work, we present a Lean 4 library for quantum information, designed as a reusable formal infrastructure for theoretical analysis. As a central demonstration of the library, we formalize the DPI for the sandwiched R'enyi relative entropy for positive semidefinite operators on finite-dimensional quantum systems. The library provides a basis-independent operator-theoretic framework for finite-dimensional quantum mechanics compatible with the standard mathematical library Mathlib, including reusable interfaces for finite-dimensional systems, states, channels, tensor products, partial traces, Choi operators, Kraus representations, and Stinespring representations. It also builds infrastructure for noncommutative trace inequalities, including operator monotonicity and convexity via the real continuous functional calculus, block-operator positivity, Hilbert-Schmidt operator spaces, Jensen's operator inequality, generalized perspectives, operator power means, and Lieb-Ando trace inequalities. On top of this framework, we formalize entropy-specific ingredients for the DPI: variational formulas for the sandwiched quasi-entropy via Young and reverse-Young inequalities, tensor-product compatibility of real powers, and Haar measures on unitary groups. Together, these components yield a Lean formalization of the DPI, give strong subadditivity as a corollary, and provide the last missing component needed to complete the Lean formalization of the generalized quantum Stein's lemma. More broadly, the development provides machine-checkable foundations for future formalized and AI-assisted research in quantum information theory.