AI 中文总结
研究在Lean中对肖尔算法及其变体进行形式化，采用智能形式化方法让软件代理分析、编写代码及修复证明，建立数学基础用于分析RSA - 2048和P - 256加密设置下的量子攻击，为量子密码分析及算法设计验证助力。
AI 中文摘要
大语言模型越来越多地协助完成要求苛刻的形式定理证明任务，特别是基于如Lean这样的机器检查库。智能系统通过搜索、重用和扩展现有形式化发展来揭示新发现，进一步推动这一过程。在量子计算中，肖尔算法及其变体对Lean形式化来说是极具挑战性的案例。本文通过智能形式化在Lean中对该算法家族进行形式化：软件代理分析来源、编写Lean代码并修复证明，由人类审查科学声明并对最终的形式证明进行机器检查。我们的形式化建立了在两种加密设置下分析量子攻击的数学基础：RSA - 2048中的2048位模数和256位素数域上的标准化椭圆曲线（P - 256）。为支持这些分析，形式化范围从用于阶数查找的量子算法到用于模运算和椭圆曲线运算的可逆量子电路。基于相关文献，我们分别对RSA - 2048和P - 256的逻辑资源估计进行形式化，并提供经典运算的额外估计。我们期望这些结果为更广泛的机器检查量子密码分析铺平道路，并代表朝着人工智能辅助的量子算法设计和验证迈出的一步。
英文摘要
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.
Comments21 pages, including appendix; 2 figures
