Global architecture of 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 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.
Chengkai Zhu
PhD Student (2023)
I obtained my BS in Applied Mathematics from China Agricultural University under the supervision of Prof. Zhencai Shen. I obtained my MS degree in Cyberspace Security from University of Chinese Academy of Sciences under the supervision of Prof. Zhenyu Huang. My research interests include quantum information theory and quantum computation.
Ziao Tang
PhD Student (co, 2025)
I obtained my BSc in Mathematics from the University of Hong Kong. My research interests include quantum information and quantum computing.
Guocheng Zhen
PhD Student (2025)
I have received my bachelor's degree in mathematics from Wuhan University in 2022 and my master's degree in mathematics from Wuhan University in 2025. My main research is about probability theory, especially Large Random Dimension Matrices Theory. I am exploring the mathematical foundation in quantum information under the guidance of Prof. Xin Wang and Prof. Bartosz Regula.
Yimeng Cao
Research Assistant
I obtained my BSc in Information and Computing Science from Huazhong Agricultural University. I am currently pursuing my MSc in Probability and Mathematical Statistics at Harbin Institute of Technology under the supervision of Prof. Ke Li. My research interests include quantum information theory, quantum resource theory.
Ranyiliu Chen
Visiting Scholar
I received my doctorate in Mathematics from the University of Copenhagen in 2025, under the supervision of Prof. Laura Mancinska. Previously I obtained my master’s and bachelor’s degrees in 2020 and 2017 respectively, both in electronic engineering from Beihang University. My research interests include quantum information theory, Bell non-locality and quantum machine learning.
Lei Zhang
PhD Student (2023)
I obtained my BMath in AMath, CO & joint PMath from the University of Waterloo. My research interests include quantum algorithm design and quantum machine learning.
Xin Wang
Associate Professor
Prof. Xin Wang founded the QuAIR Lab at HKUST (Guangzhou) in June 2023. His research aims to advance our understanding of the limits of information processing with quantum systems and the potential of quantum artificial intelligence. His current interests include quantum algorithms, quantum resource theory, quantum machine learning, quantum computer architecture, and quantum error processing. Prior to establishing the QuAIR Lab, Prof. Wang was a Staff Researcher at the Institute for Quantum Computing at Baidu Research, where he focused on quantum computing research and the development of the Baidu Quantum Platform. Notably, he led the development of Paddle Quantum, a Python library for quantum machine learning. From 2018 to 2019, he was a Hartree Postdoctoral Fellow at the Joint Center for Quantum Information and Computer Science (QuICS) at the University of Maryland, College Park. Prof. Wang received his Ph.D. in quantum information from the University of Technology Sydney in 2018, under the supervision of Prof. Runyao Duan and Prof. Andreas Winter. He obtained his B.S. in mathematics (Wu Yuzhang Honors) from Sichuan University in 2014.