近日，量子计算复杂性理论中备受关注的Aaronson-Ambainis猜想正式获得证明。该成果由PSI机构开发的研究系统基于Anthropic模型完成，并同步给出了在Lean证明助手中的完整形式化验证。这一猜想聚焦量子计算机在随机输入场景下相对经典计算机的加速能力边界。最新证明表明，量子计算机在随机输入上并不存在指数级加速，从而为量子优势的适用范围划定了更清晰的理论界限。该结果解决了量子计算领域长期悬而未决的重要问题，也展示了人工智能辅助数学证明与形式化验证在高难理论研究中的潜力，对判断量子算法在通用或平均情况下的实际优势具有重要参考价值。