Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory

• URL: http://arxiv.org/abs/2607.09632v1
• Date: Fri, 10 Jul 2026 17:28:26 GMT
• Title: Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory
• Abstract summary: Quantum information theory (QIT) characterizes the capabilities and fundamental limits of quantum information processing.<n>Existing developments lack a reusable operational layer that defines codes, error criteria, achievable rates, and capacities.<n>We present LeanQIT, a Lean 4 library for finite-dimensional QIT.
• Score: 13.58013986113788
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Quantum information theory (QIT) characterizes the capabilities and fundamental limits of quantum information processing, underpinning quantum communication, computation, and error correction. Formalizing its coding theorems requires connecting finite-block protocols, analytic inequalities, and asymptotic limits within a unified machine-checked framework. Existing developments, however, lack a reusable operational layer that defines codes, error criteria, achievable rates, and capacities independently of their information-theoretic characterizations. In this work, we present LeanQIT, a Lean 4 library for finite-dimensional QIT. It provides composable, kernel-checked interfaces for quantum states and channels, source and channel codes, finite-block performance criteria, hypothesis testing, one-shot quantities, and asymptotic rate constructions. Using this infrastructure, we formalize Schumacher's quantum source-coding theorem, the Holevo--Schumacher--Westmoreland classical-capacity theorem, and the entanglement-assisted classical-capacity theorem together with its strong converse. By separating operational definitions from analytic characterizations and exposing reusable achievability, converse, and asymptotic components, Lean-QIT provides a machine-readable foundation for formal QIT and a compositional knowledge substrate for emerging AI-assisted formalization, automated proof search, and agentic reasoning in quantum information and computation.

Related papers

• AQER: a scalable and efficient data loader for digital quantum computers [62.40228216126285]
  We develop AQER, a scalable AQL method that constructs the loading circuit by systematically reducing entanglement in target states.<n>We conduct systematic experiments to evaluate the effectiveness of AQER, using synthetic datasets, classical image and language datasets, and a quantum many-body state datasets with up to 50 qubits.
  arXiv  Detail & Related papers  (2026-02-02T14:39:42Z)
• Symbolic Specification and Reasoning for Quantum Data and Operations [5.341843260877702]
  We present a general logical framework, called Operator Logic $mathbfSOL$, which enables symbolic specification and reasoning about quantum data and operations.<n>Within this framework, a classical first-order logical language is embedded into a language of formal operators used to specify quantum data and operations.<n>This embedding allows reasoning about their properties modulo a chosen theory of the underlying classical data.
  arXiv  Detail & Related papers  (2025-12-26T20:57:42Z)
• Quantumness certification via non-demolition measurements [0.0]
  Quantum Non-Demolition Measurements (QNDM) serve as the appropriate instrument for this certification.<n>We discuss an application where the quantum-to-classical transition due to the interaction with an environment can be tracked by QNDM.<n>Because of its straightforward implementation, the QNDM approach can be of direct relevance to both the foundations of quantum mechanics and quantum information theory.
  arXiv  Detail & Related papers  (2025-12-10T15:15:10Z)
• Quantum Machine Unlearning: Foundations, Mechanisms, and Taxonomy [9.347709392900502]
  Quantum Machine Unlearning has emerged as a foundational challenge at the intersection of quantum information theory privacypreserving computation and trustworthy artificial intelligence.<n>This paper advances QMU by establishing a formal framework that unifies physical constraints algorithmic mechanisms and ethical governance within a verifiable paradigm.
  arXiv  Detail & Related papers  (2025-11-01T05:11:40Z)
• Advances in Machine Learning: Where Can Quantum Techniques Help? [0.0]
  Quantum Machine Learning (QML) represents a promising frontier at the intersection of quantum computing and artificial intelligence.<n>This review explores the potential of QML to address the computational bottlenecks of classical machine learning.
  arXiv  Detail & Related papers  (2025-07-11T07:47:47Z)
• VQC-MLPNet: An Unconventional Hybrid Quantum-Classical Architecture for Scalable and Robust Quantum Machine Learning [50.95799256262098]
  Variational quantum circuits (VQCs) hold promise for quantum machine learning but face challenges in expressivity, trainability, and noise resilience.<n>We propose VQC-MLPNet, a hybrid architecture where a VQC generates the first-layer weights of a classical multilayer perceptron during training, while inference is performed entirely classically.
  arXiv  Detail & Related papers  (2025-06-12T01:38:15Z)
• Separable Power of Classical and Quantum Learning Protocols Through the Lens of No-Free-Lunch Theorem [70.42372213666553]
  The No-Free-Lunch (NFL) theorem quantifies problem- and data-independent generalization errors regardless of the optimization process. We categorize a diverse array of quantum learning algorithms into three learning protocols designed for learning quantum dynamics under a specified observable. Our derived NFL theorems demonstrate quadratic reductions in sample complexity across CLC-LPs, ReQu-LPs, and Qu-LPs. We attribute this performance discrepancy to the unique capacity of quantum-related learning protocols to indirectly utilize information concerning the global phases of non-orthogonal quantum states.
  arXiv  Detail & Related papers  (2024-05-12T09:05:13Z)
• An operational definition of quantum information scrambling [0.0]
  Quantum information scrambling (QIS) is a characteristic feature of several quantum systems. We propose a novel and computationally efficient QIS quantifier based on a formulation of QIS in terms of quantum state discrimination. We show that the optimal guessing probability, which reflects the degree of QIS induced by an isometric quantum evolution, is directly connected to the accessible min-information.
  arXiv  Detail & Related papers  (2023-12-18T19:00:01Z)
• Potential and limitations of quantum extreme learning machines [55.41644538483948]
  We present a framework to model QRCs and QELMs, showing that they can be concisely described via single effective measurements. Our analysis paves the way to a more thorough understanding of the capabilities and limitations of both QELMs and QRCs.
  arXiv  Detail & Related papers  (2022-10-03T09:32:28Z)
• Quantum Semantic Communications for Resource-Efficient Quantum Networking [52.3355619190963]
  This letter proposes a novel quantum semantic communications (QSC) framework exploiting advancements in quantum machine learning and quantum semantic representations. The proposed framework achieves approximately 50-75% reduction in quantum communication resources needed, while achieving a higher quantum semantic fidelity.
  arXiv  Detail & Related papers  (2022-05-05T03:49:19Z)
• Using Quantum Metrological Bounds in Quantum Error Correction: A Simple Proof of the Approximate Eastin-Knill Theorem [77.34726150561087]
  We present a proof of the approximate Eastin-Knill theorem, which connects the quality of a quantum error-correcting code with its ability to achieve a universal set of logical gates. Our derivation employs powerful bounds on the quantum Fisher information in generic quantum metrological protocols.
  arXiv  Detail & Related papers  (2020-04-24T17:58:10Z)

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.