谷歌 LLM 智能体团队发现经 Lean 证明的量子程序，一项例程成本降低 290 倍

为何重要

大型量子算法无法在当今的经典或量子计算机上测试，因此依赖数值检验的 AI 搜索只能停留在小规模实例。作者在 Lean 定理证明器中构建了量子程序库，让多支 LLM 智能体团队提出程序，并由独立验证器依据冻结的规格核查每一份正确性与成本证明。各团队通过共享维基和定期虚拟会议交流成果。接下来要看这些资源节省能否经受独立评审，以及 Lean 程序库是否对外开放。