{"ID":6497576,"CreatedAt":"2026-07-13T01:19:40.13847098Z","UpdatedAt":"2026-07-14T01:36:59.12045529Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2607.09632","arxiv_id":"2607.09632","title":"Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory","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.","short_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...","url_abs":"https://arxiv.org/abs/2607.09632","url_pdf":"https://arxiv.org/pdf/2607.09632v1","authors":"[\"Chengkai Zhu\",\"Ziao Tang\",\"Guocheng Zhen\",\"Yimeng Cao\",\"Yusheng Zhao\",\"Ranyiliu Chen\",\"Xuanqiang Zhao\",\"Lei Zhang\",\"Xin Wang\"]","published":"2026-07-10T17:28:26Z","proceeding":"quant-ph","tasks":"[\"quant-ph\",\"cs.AI\"]","methods":"[]","has_code":false}