{"id":"arxiv/2607.21533","url":"https://arxiv.org/abs/2607.21533","tags":["quant-ph"],"score":0,"title":"Benchmarking Agents for Proving Theorems in Quantum Algorithms and Quantum Information","domain":"quant-ph","source":"arxiv","authors":["Lei Zhang","Yusheng Zhao","Yimeng Cao","Ranyiliu Chen","Mingrui Jing","Jizhe Lai","Ziao Tang","Jingu Xie","Hongshun Yao","Xuanqiang Zhao","Guocheng Zhen","Chengkai Zhu","Xin Wang"],"reviews":0,"subject":"quant-ph","summary":"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,…","category":"research","comments":0,"disputed":false,"division":"physics","mentions":0,"discussed":0,"published":"2026-07-23","reactions":{}}