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

Jul 16, 2026

Upload by Ophelia

Quantum information theory (QIT) establishes both the capabilities and fundamental limits of quantum information processing, supporting quantum communication, computation, and error correction. Formalizing coding theorems requires connecting finite-block protocols, analytic inequalities, and asymptotic limits within a unified machine-checked framework. Existing work lacks a reusable operational layer defining codes, error criteria, achievable rates, and capacities independently of analytic characterizations. Lean-QIT is a Lean 4 library for finite-dimensional QIT with kernel-checked composable interfaces, enabling machine-readable formalizations of core theorems and reusable achievability/converse/asymptotic components.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages29

Reading Time1 h 13 min

Introduction

Lean-QIT Architecture

Finite-Dimensional QIT Building Blocks

Typed states and channels

Subsystem, classical, and measurement calculus

State geometry and purification interfaces

Information quantities and data processing

Testing interfaces for finite-block converses

One-shot and asymptotic bridges

Coding Spine of Quantum Shannon Theory

Schumacher Source Coding

Classical Capacity

Entanglement-assisted classical capacity

Conclusion

A Selected Public Endpoint Wrappers

Fully quantum AEP endpoint

HSW source-facing package

Entanglement-assisted asymptotic endpoints

arXiv :2607 .09632v1 [ quant-ph] 10 Jul 2026 Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory Chengkai Zhu∗ 1 , Ziao Tang†2, Guocheng Zhen2 , Yimeng Cao2 , Yusheng Zhao 1,2 , Ranyiliu Chen3 , Xuanqiang Zhao4,1 , Lei Zhang‡1,2, and Xin Wang§2 1 QudeLeap Research, Shanghai 200030, China 2 The Hong Kong University of Science and Technology (Guangzhou), Guangdong 511453, China 3 Quantum Science Center of Guangdong-Hong Kong-Macao Greater Bay Area, Shenzhen 518045, China 4 The University of Hong Kong, Pokfulam Road, Hong Kong [github.com/QuAIR/Lean-QIT](github.com/QuAIR/Lean-QIT) 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 Lean-QIT, 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. 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. Contents 1 Introduction 2 2 Lean-QIT Architecture 3 3 Finite-Dimensional QIT Building Blocks 4 3.1 Typed states and channels . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 3.2 Subsystem, classical, and measurement calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.3 State geometry and purification interfaces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.4 Information quantities and data processing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.5 Testing interfaces for finite-block converses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 3.6 One-shot and asymptotic bridges . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 4 Coding Spine of Quantum Shannon Theory 13 4.1 Schumacher Source Coding . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 4.2 Classical Capacity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 4.3 Entanglement-assisted classical capacity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 5 Conclusion 23 ∗ [zhuchengkai7@gmail.com](zhuchengkai7@gmail.com)[ ](zhuchengkai7@gmail.com)† [zatang004@gmail.com](zatang004@gmail.com)[ ](zatang004@gmail.com)‡ [leizhang116.4@gmail.com](leizhang116.4@gmail.com) § [felixxinwang@hkust-gz.edu.cn](felixxinwang@hkust-gz.edu.cn) A Selected Public Endpoint Wrappers 25 A.1 Fully quantum AEP endpoint . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 A.2 HSW source-facing package . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 A.3 Entanglement-assisted asymptotic endpoints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 Introduction Quant

FAQs

What problem does Lean-QIT address in formalizing quantum information theory?

Lean-QIT addresses the lack of a reusable operational layer that can define quantum codes, error criteria, achievable rates, and capacities in a way that is independent from analytic characterizations.

What kinds of interfaces does Lean-QIT provide 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.

Which quantum Shannon theory results does the library formalize?

Using the infrastructure, Lean-QIT formalizes Schumacher’s quantum source-coding theorem, the Holevo–Schumacher–Westmoreland classical capacity theorem, and the entanglement-assisted classical capacity theorem.

Jul 16, 2026

Upload by Ophelia