From the 3 of 11 linked papers with an AI index.
11 papers
Benchmarking Agents for Proving Theorems in Quantum Algorithms and Quantum Information
Lei Zhang, Yusheng Zhao, Yimeng Cao +10
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.…
Building Shor's Algorithm in Lean: An Agentic Formalization of Quantum Attacks on RSA-2048 and P-256
Lei Zhang, Yusheng Zhao, Hongshun Yao +1
The paper uses AI‑driven agents together with the Lean theorem prover to formally verify Shor's algorithm and its quantum attacks on RSA‑2048 and the P‑256 elliptic curve, providin…
An Agentic Formalization for Certified Quantum Neural Network Design
Mingrui Jing, Lei Zhang, Yusheng Zhao +2
The paper formalizes the theory of quantum neural networks (QNNs) using a machine-checked Lean 4 development, providing exact characterizations of expressivity and trainability and…
Quantum Imaginary-Time Evolution with Polynomial Resources in Evolution Time
Lei Zhang, Jizhe Lai, Xian Wu +1
The paper proposes a quantum algorithm that efficiently prepares imaginary-time evolved states with polynomial resources in evolution time, using an adaptive normalization factor t…
Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory
Chengkai Zhu, Ziao Tang, Guocheng Zhen +6
Quantum information theory (QIT) characterizes the capabilities and fundamental limits of quantum information processing, underpinning quantum communication, computation, and error…
Shadow-Based Noise Fingerprinting of Simulated Quantum Noise Models
Vridhi Jain, Lei Zhang
Accurate noise classification is essential for operating near-term quantum processors, yet existing approaches, such as quantum process tomography, scale exponentially with system…