A result comparison for verifying Shor’s factoring algorithm.Abstract
Formal verification is becoming increasingly practical for quantum computing, yet the ability of AI agents to construct machine-checkable proofs in this domain remains unmeasured. We introduce Lean-QuantumAlg-Bench and Lean-QIT-Bench, two Lean 4 benchmarks containing 36 and 40 theorem-completion tasks for quantum algorithms and quantum information theory, respectively. Every task compiles in a fixed environment and is evaluated by deterministic proof checking and targeted semantic review, with difficulty weights assigned before model execution. We evaluate four models-GPT-5.5, Kimi K3, DeepSeek V4-Pro, and MiniMax M3-within a common theorem-proving framework under two settings: a task-only baseline and library-augmented deduction (LAD), which additionally provides access to a verified domain library. The highest difficulty-weighted scores are 60.4 out of 100 on the quantum-algorithm benchmark and 59.6 out of 100 on the quantum-information benchmark. LAD improves both score and completion rate in all eight model-benchmark comparisons, with gains of up to 15.9 points, providing evidence that verified libraries can strengthen domain-specific proof agents. The results reveal recurring weaknesses of agentic proving in areas such as quantum simulation, quantum learning, quantum information measures, and entanglement theory. Monetary and wall-clock costs per score point also vary substantially across models, highlighting important capability-efficiency trade-offs. We expect these benchmarks to establish a reproducible baseline for developing more capable and reliable proof agents, and to pave the way toward self-evolving AI scientists for advancing quantum information science.
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.
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.
Jizhe Lai
PhD Student (2025)
I obtained my BS in Physics from SUN YAT-SEN University under the supervision of Prof. Yiwen Pan. I obtained my MS degree in Imperial College London under the supervision of Prof. Chris Hull, FRS. My research interests include mathematical physics 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.
Jingu Xie
PhD Student (2026)
I am currently studying at the Quantum AI Research Lab, Thrust of Artificial Intelligence, Information Hub, The Hong Kong University of Science and Technology (Guangzhou). My research interests include quantum information theory, quantum computation, and applied mathematics.
Hongshun Yao
PhD Student (2024)
I obtained my BS degree in Mathematics from Nanjing University of Aeronautics and Astronautics and my MS degree in Mathematics from Beihang University. My research interests include quantum information theory and quantum machine learning.
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.
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.
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.