Building Shor's Algorithm in Lean: An Agentic Formalization of Quantum Attacks on RSA-2048 and P-256

Abstract

Large language models are increasingly assisting with demanding formal theorem-proving tasks, particularly when grounded in machine-checked libraries such as Lean. Agentic systems further amplify this process by searching, reusing, and extending existing formal developments to uncover new discoveries. In quantum computing, Shor’s algorithm and its variants present such a demanding case for Lean formalization. In this work, we formalize this algorithm family in Lean through agentic formalization: software agents analyze sources, write Lean code and repair proofs, with human review of the scientific claims and machine checking of the resulting formal proofs. Our formalization develops the mathematical foundations for analyzing quantum attacks in two cryptographic settings: a 2048-bit modulus in the RSA-2048 and the standardized elliptic curve over a 256-bit prime field (P-256). To support these analyses, the formalization ranges from quantum algorithms for order finding to reversible quantum circuits for modular and elliptic-curve arithmetic. Based on [Quantum 5, 433] and [ASIACRYPT 2017, 241–270], we formalize the logical resource estimates for RSA-2048 and P-256, respectively, and provide additional estimates of classical operations. We expect the results pave the way for broader machine-checked quantum cryptanalysis and represent a step toward AI-assisted design and verification of quantum algorithms.

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.

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.

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.