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

• URL: http://arxiv.org/abs/2607.05492v1
• Date: Mon, 06 Jul 2026 18:00:00 GMT
• Title: Lean-Quantum: Toward AI-Assisted Formalization of Quantum Information
• Abstract summary: We present a Lean 4 library for quantum information, designed as a reusable formal infrastructure for theoretical analysis.<n>We formalize the DPI for the sandwiched Rényi relative entropy for positive semidefinite operators on finite-dimensional quantum systems.<n>The library provides a basis-independent operator-theoretic framework for finite-dimensional quantum mechanics.
• Score: 4.962621441807053
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Quantum information theory is built on entropic quantities; among them, the sandwiched Rényi 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ényi 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.

Related papers

• Quantum Information Decoupling Beyond Finite Dimensions [1.2691047660244335]
  We establish a framework for arbitrary separable, possibly infinite-dimensional systems.<n>For finite-dimensional inputs, we assume finite entropy of the manipulated system.<n>As an application, we construct an infinite-dimensional quantum-state-merging protocol.
  arXiv  Detail & Related papers  (2026-07-28T18:00:00Z)
• Quantum Reservoir Computing: Recent Advances and Future Directions [34.77938621771246]
  Quantum reservoir computing (QRC) uses the dynamics of a fixed or weakly tuned quantum system to transform temporal and sequential inputs into measured features.<n>Its computational power is often attributed to the exponentially large Hilbert space of the quantum system.<n>On hardware, these capabilities are further constrained by finite sampling, hardware noise, measurement backaction, and the cost of estimating observables.
  arXiv  Detail & Related papers  (2026-07-20T22:38:49Z)
• Device-independent Quantum Key Distribution in the commuting operator framework [10.668771582679561]
  Device-independent quantum key distribution (DIQKD) is arguably the gold standard for secure quantum communication.<n>Existing proof techniques do not always meet this goal as they tend to rely on subtile assumptions.<n>We show that task of computing key rates can be casted as a non-commutative optimization problem.
  arXiv  Detail & Related papers  (2026-07-03T19:44:10Z)
• Cumulant-based quantum relative Rényi functional [0.0]
  We introduce a new cumulant-based quantum relative Rényi functional as a candidate quantum Rényi divergence.<n>The functional naturally admits a path-integral-like representation through the Lie-Trotter product expansion.<n>We show that the resulting relative quantumness quantity vanishes if and only if the underlying states commute.
  arXiv  Detail & Related papers  (2026-06-30T06:34:53Z)
• Geometric Complexity of Quantum Channels via Unitary Dilations [0.0]
  We introduce and analyze a geometric complexity functional for families of quantum channels based on unitary dilations.<n>We quantify the loss of geometric complexity relative to a prescribed ideal closed evolution.
  arXiv  Detail & Related papers  (2026-01-02T16:28:36Z)
• Performance Guarantees for Quantum Neural Estimation of Entropies [31.955071410400947]
  Quantum neural estimators (QNEs) combine classical neural networks with parametrized quantum circuits.<n>We study formal guarantees for QNEs of measured relative entropies in the form of non-asymptotic error risk bounds.<n>Our theory aims to facilitate principled implementation of QNEs for measured relative entropies.
  arXiv  Detail & Related papers  (2025-11-24T16:36:06Z)
• Grassmann Variational Monte Carlo with neural wave functions [45.935798913942904]
  We formalize the framework introduced by Pfau et al.citepfau2024accurate in terms of Grassmann geometry of the Hilbert space.<n>We validate our approach on the Heisenberg quantum spin model on the square lattice, achieving highly accurate energies and physical observables for a large number of excited states.
  arXiv  Detail & Related papers  (2025-07-14T13:53:13Z)
• Quantum computer formulation of the FKP-operator eigenvalue problem for probabilistic learning on manifolds [0.0]
  We present a quantum computing formulation to address a challenging problem in the development of probabilistic learning on manifold (PLoM)<n>It involves solving the spectral problem of the high-dimensional Fokker-Planck operator, which remains beyond the reach of classical computing.<n>Explicit formulas for the Laplacian and potential are derived and mapped onto qubits using Pauli matrix expressions.
  arXiv  Detail & Related papers  (2025-02-20T14:05:16Z)
• DimINO: Dimension-Informed Neural Operator Learning [41.37905663176428]
  DimINO is a framework inspired by dimensional analysis.<n>It can be seamlessly integrated into existing neural operator architectures.<n>It achieves up to 76.3% performance gain on PDE datasets.
  arXiv  Detail & Related papers  (2024-10-08T10:48:50Z)
• Quantum channels, complex Stiefel manifolds, and optimization [45.9982965995401]
  We establish a continuity relation between the topological space of quantum channels and the quotient of the complex Stiefel manifold. The established relation can be applied to various quantum optimization problems.
  arXiv  Detail & Related papers  (2024-08-19T09:15:54Z)
• Quantum tomography of helicity states for general scattering processes [55.2480439325792]
  Quantum tomography has become an indispensable tool in order to compute the density matrix $rho$ of quantum systems in Physics. We present the theoretical framework for reconstructing the helicity quantum initial state of a general scattering process.
  arXiv  Detail & Related papers  (2023-10-16T21:23:42Z)
• A Lie Algebraic Theory of Barren Plateaus for Deep Parameterized Quantum Circuits [37.84307089310829]
  Variational quantum computing schemes train a loss function by sending an initial state through a parametrized quantum circuit. Despite their promise, the trainability of these algorithms is hindered by barren plateaus. We present a general Lie algebra that provides an exact expression for the variance of the loss function of sufficiently deep parametrized quantum circuits.
  arXiv  Detail & Related papers  (2023-09-17T18:14:10Z)
• Noisy Quantum Kernel Machines [58.09028887465797]
  An emerging class of quantum learning machines is that based on the paradigm of quantum kernels. We study how dissipation and decoherence affect their performance. We show that decoherence and dissipation can be seen as an implicit regularization for the quantum kernel machines.
  arXiv  Detail & Related papers  (2022-04-26T09:52:02Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.