Building Shor's Algorithm in Lean: An Agentic Formalization of Quantum Attacks on RSA-2048 and P-256
Formalized Shor's algorithm in Lean, providing detailed resource estimates for RSA-2048 and P-256 quantum attacks, enabling machine-verified cryptanalysis.
Key Findings
Methodology
This work employs agentic formalization within Lean, integrating quantum information theory and mathematical libraries. Software agents automate literature retrieval, code generation, and proof repair, combining human review for scientific accuracy. The formalization models quantum order finding, reversible circuits for modular and elliptic-curve arithmetic, and classical post-processing. Using quantum phase estimation and continued fractions, the approach estimates the period with resource metrics—qubits, gates, depth—quantitatively. The process ensures rigorous, reusable proofs, bridging quantum algorithms and cryptographic applications, with resource bounds validated through machine-checked proofs.
Key Results
- For RSA-2048, formalization indicates success probability ≥2/3, requiring 6.19×10^3 logical qubits, 8.1×10^9 Toffoli gates, and circuit depth of 6.42×10^9, with classical operations around 3.69×10^4. This demonstrates feasible resource bounds for quantum factorization at realistic scales.
- In P-256 elliptic-curve discrete logarithm, success probability ≥2/3, with 2.33×10^3 qubits, 1.26×10^11 Toffoli gates, and depth 1.16×10^11, confirming the practicality of quantum scalar recovery within these parameters.
- Both results leverage quantum phase estimation and reversible arithmetic, with classical post-processing for key recovery, providing a comprehensive, machine-verified resource framework for quantum cryptanalysis.
Significance
This research pioneers the complete formalization of Shor’s algorithm in Lean, delivering precise resource estimates for cryptographically relevant instances. It advances the automation and rigor of quantum algorithm verification, addressing long-standing challenges in cryptanalysis and quantum computing security assessments. The integration of agentic workflows and machine-checked proofs enhances trustworthiness, paving the way for scalable, automated quantum cryptanalysis tools. The work significantly impacts both theoretical and applied quantum cryptography, offering a foundational framework for future security evaluations and hardware development aligned with realistic resource constraints.
Technical Contribution
The study introduces a systematic formalization of quantum order finding and elliptic-curve discrete logarithm within Lean, combining quantum algorithms, reversible circuit design, and classical post-processing into a unified, machine-verified framework. It innovates with agentic workflows for automated literature integration, code synthesis, and proof repair, ensuring scalability. The resource estimation employs logical qubits, Toffoli gates, and circuit depth metrics, providing concrete bounds directly applicable to hardware considerations. This comprehensive approach bridges theoretical quantum algorithms and practical cryptanalysis, establishing new standards for formal verification in quantum computing.
Novelty
This is the first comprehensive formalization of Shor’s algorithm covering both RSA-2048 factorization and P-256 discrete logarithm within Lean, integrating quantum and classical components with explicit resource bounds. The agentic formalization workflow enhances automation, reproducibility, and trustworthiness, surpassing prior partial verifications. The detailed resource estimates and end-to-end proofs establish a new benchmark for machine-verified quantum cryptanalysis, enabling systematic security assessments and algorithm design in a formal setting.
Limitations
- The current models do not incorporate quantum noise, error correction, or fault tolerance, which are critical for real hardware implementation, potentially increasing resource requirements significantly.
- Resource estimates are based on idealized logical circuits, not accounting for physical qubit overheads, error rates, or hardware-specific constraints.
- Success probabilities are quantified under ideal assumptions; actual hardware imperfections could reduce effectiveness, necessitating further robustness analysis.
Future Work
Future efforts will incorporate error correction, fault-tolerant architectures, and noise models to refine resource estimates. Extending formalization to other cryptographic primitives and algorithms will broaden applicability. Developing automated tools for end-to-end verification of quantum algorithms, integrating physical constraints, and optimizing circuit designs are key directions. These advancements aim to make quantum cryptanalysis more practical and trustworthy, ultimately guiding hardware development and security standards.
AI Executive Summary
This work presents a comprehensive formalization of Shor’s quantum algorithm within the Lean proof assistant, targeting cryptographically significant problems such as RSA-2048 factorization and P-256 elliptic-curve discrete logarithm. Leveraging an agentic workflow, researchers automated the retrieval of relevant literature, generated formal code, and iteratively refined proofs, ensuring rigorous correctness and reusability. The core technical innovation lies in modeling quantum order finding via phase estimation and continued fractions, alongside reversible circuits for modular and elliptic-curve arithmetic. These components are integrated into a unified framework that quantifies resource requirements—logical qubits, Toffoli gates, and circuit depth—at a detailed level. For RSA-2048, the formalization indicates that a quantum attack can succeed with probability at least 2/3 using approximately 6,190 qubits, 8.1 billion Toffoli gates, and a circuit depth of 6.42 billion, with classical post-processing steps around 36,900 operations. Similarly, for P-256, the resource estimates are 2,330 qubits, 126 billion gates, and a depth of 116 billion, also achieving the success threshold. These results demonstrate that such quantum attacks are within the realm of theoretical feasibility, given current resource estimates, and provide a detailed, machine-verified foundation for future cryptanalysis. The formalization bridges the gap between abstract quantum algorithms and practical cryptographic threats, offering a scalable, automated platform for analyzing quantum vulnerabilities. Future work aims to incorporate noise models, error correction, and hardware constraints, further refining resource estimates and extending the framework to additional cryptographic primitives. Overall, this research significantly advances the state of formal quantum cryptanalysis, establishing a new standard for machine-verified security assessments and algorithm design.
Deep Analysis
Background
量子算法的形式化研究逐步从抽象模型向实际实现过渡。早期工作如Qiskit和QuTiP主要关注模拟验证，随后出现Q#、Coq、Qafny等工具，增强了算法的严密性。近年来，随着量子硬件逐步成熟，形式验证成为确保算法正确性和资源合理性的关键手段。特别是在密码学领域，Shor算法的潜在威胁促使学界关注其严密的理论基础。已有部分验证工作如Qbricks、CoqQ验证了子模块，但缺乏端到端的完整验证。本研究利用Lean平台，结合量子信息理论和代理人自动化，首次实现了完整的Shor算法形式化，涵盖阶寻找、可逆电路设计和成功概率估算，为未来量子密码分析提供了坚实基础。
Core Problem
量子算法在密码破解中的潜力巨大，但其复杂性和硬件限制使得验证变得困难。现有方法多为模拟或部分验证，缺乏系统化的端到端证明。特别是在RSA-2048和P-256场景，资源需求巨大，缺乏精确的量化分析。如何在保证严密性和自动化的基础上，准确估算实现所需的逻辑资源，是当前的核心难题。解决这一问题对于评估量子威胁、指导硬件设计具有重要意义。
Innovation
本研究的创新点包括：1）引入代理人机制，实现文献检索、代码生成和证明修正的自动化；2）在Lean中系统化建立了阶寻找、可逆算术和成功概率的完整模型；3）结合逻辑资源模型，提供了详细的比特数、门数和深度估算；4）实现了RSA-2048和P-256两大密码场景的端到端验证，填补了形式化验证的空白。这些创新极大提升了量子算法验证的自动化水平，为未来量子密码分析提供了可扩展的框架。
Methodology
- �� 代理人检索相关文献和资料，分析Shor算法的关键组成部分。• 编写Lean代码实现阶寻找、可逆电路设计和成功概率估算。• 利用量子相位估计和连续分数法实现阶数的高效估算。• 构建逻辑资源模型，量化所需比特数、门数和电路深度。• 结合人工审查和机器验证，确保模型的严密性和正确性。• 通过多轮试验，验证模型在RSA-2048和P-256场景的适用性。• 进行资源估算和成功概率分析，形成完整的理论框架。
Experiments
采用RSA-2048的模数和P-256椭圆曲线参数作为输入，利用Lean formalization验证阶寻找和离散对数的成功概率。通过模拟不同资源限制下的电路设计，评估所需的逻辑比特、门数和深度。对比已有的非正式估算，验证模型的准确性和实用性。多次重复试验确保成功概率≥2/3，统计资源消耗，分析其在实际量子硬件上的可行性。
Results
在RSA-2048场景中，formalization显示实现成功概率≥2/3，资源需求为6.19×10^3比特、8.1×10^9门、深度6.42×10^9，经典操作3.69×10^4。P-256场景中，资源需求为2.33×10^3比特、1.26×10^11门、深度1.16×10^11，成功概率同样≥2/3。这些结果提供了量子攻击的详细资源估算，为硬件设计和安全评估提供了理论依据。
Applications
该形式化模型可用于评估未来量子计算机对RSA和椭圆曲线密码的威胁，为密码系统的安全参数设计提供量化依据。同时，为量子算法的自动化验证和优化提供了平台基础，有助于推动量子密码学的标准化和产业化。
Limitations & Outlook
模型未考虑量子电路中的噪声和误差校正，实际硬件实现可能需要更高资源。资源估算基于理想化的逻辑电路，未充分考虑物理实现复杂性。算法成功概率虽已量化，但在极端资源限制下的实际表现仍需实验证明。未来需结合容错机制，优化电路设计以降低成本。
Plain Language Accessible to non-experts
想象你在一个工厂里，试图找到一批隐藏的宝藏。传统方法像用手工逐个检查，每次都要花费很多时间。而量子算法就像有一台超级智能的机器人，它可以同时检查很多地方，快速找到宝藏的线索。Shor算法就是这样一台机器人，它利用量子“叠加”和“干涉”原理，能在极短时间内找到隐藏的秘密，比如密码背后的数字。这个过程看似神奇，但实际上是通过复杂的数学和电路设计实现的。研究人员用Lean这个“工厂的蓝图”工具，把这些复杂的步骤变成可以验证的图纸，确保每一步都正确无误。这样一来，我们就能更清楚地知道未来的超级计算机可能会多快破解密码，也能提前做好防护。这个研究就像给工厂装上了智能检测器，让我们提前知道宝藏在哪里，防止被偷走。
ELI14 Explained like you're 14
想象你在玩一个超级难的拼图游戏，里面藏着一个秘密宝箱。用普通的方法，你得一块一块拼，花很长时间。而现在，想象你有一台神奇的机器，它可以同时试很多不同的拼法，几秒钟就能找到正确的拼图！这台机器用的就是量子技术，特别是一个叫Shor的算法。科学家们用一种叫Lean的工具，把这个神奇的拼图过程写成了可以验证的蓝图，确保每一步都正确无误。这样一来，我们就知道，未来的超级电脑可能在几秒钟内就能破解一些密码，就像用神奇的拼图机器找到宝藏一样。研究的目标是让我们提前知道这些密码的弱点，保护我们的信息安全。就像提前知道宝藏藏在哪里，才能更好地守住它。
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.