在Lean中构建Shor算法：对RSA-2048和P-256量子攻击的智能体形式化

大型语言模型越来越多地协助要求严格的定理证明任务，特别是当它们基于如Lean这样的机器检查库时。智能体系统通过搜索、重用和扩展现有的形式化开发来发现新发现，进一步放大了这一过程。在量子计算中，Shor算法及其变体为Lean形式化提出了这样一个高要求案例。在这项工作中，我们通过智能体形式化在Lean中形式化了这一算法族：软件智能体分析来源、编写Lean代码并修复证明，由人类审查科学主张，并由机器检查所得的形式化证明。我们的形式化开发了分析两种密码设置中量子攻击的数学基础：RSA-2048中的2048位模数和256位素数域上的标准化椭圆曲线（P-256）。为支持这些分析，形式化范围从用于求阶的量子算法到用于模运算和椭圆曲线算术的可逆量子电路。基于[Quantum 5, 433]和[ASIACRYPT 2017, 241-270]，我们分别形式化了RSA-2048和P-256的逻辑资源估计，并提供了经典操作的额外估计。我们期望这些结果为更广泛的机器检查量子密码分析铺平道路，并代表朝着AI辅助设计和验证量子算法迈出的一步。