量子 · AI 写好的量子程序，由证明器签收：算术电路报出 290 倍改进

量子算法设计的麻烦，一半在难，一半在没法试。经典代码写完跑一遍就知道对错；量子程序在今天真实的机器上根本跑不动——比特太少，噪声太大，能精确模拟的规模小得可怜。传统路线里，设计一套供容错机器使用的量子算法，要几个方向的专家凑在一起熬上几年。

11 月 6 日，Google DeepMind 的 25 人团队在 arXiv 挂出论文（编号 2611.09822），换了个思路：试不了，就证明。他们把量子算法的发现整个搬进了 Lean 定理证明器——LLM agent 对着形式化的规约合成新程序，正确性和资源开销都由证明器背书。跑不了，照样验得了。

流程值得细看。规约先行：先写清程序要满足什么性质、开销上限是多少。然后 agent 组队开工，各自合成候选；Lean 逐条验收，通过的才准进库。库里还长出了一套"科研社会"：agent 之间用 wiki 共享进展，定期开会讨论想法。论文的措辞是，这把人类智能与人工智能的协作放到了数学证明的保护之下，在大规模上同时运转。

成绩单：量子算术这一项，比既有方案报出 290 倍的改进；并行搜索 1.4 倍；聚变模拟 11 倍；光化学 8 倍；药物代谢 2.5 倍。最扎眼的是那个 290。算术电路是容错量子算法的地基——哈密顿模拟、Shor、量子化学，全都踩在它上面。地基便宜了，楼上跟着降价，而且这层便宜会与硬件进步相乘：硬件提升十倍、算术开销再压几十倍，叠出来就是几个数量级的综合账。

这条线是 DeepMind 一路铺过来的。2022 年 AlphaTensor 改写矩阵乘法，2023 年 AlphaDev 重排排序算法，2024 年 AlphaProof 冲到 IMO 奖牌线附近，2025 年 AlphaEvolve 优化各类计算内核。这次的差别就在"证明"二字。以前的发现靠基准测试说话，这次的正确性由定理证明器盖章——而量子程序恰好是最测不起的那类代码，证明是唯一的免费午餐。

硬件路线图天天上头条：比特数、保真度、纠错码。算法这条腿经常被冷落。这篇论文的杠杆是乘法性质的，作者自己的说法是"缩短通往实用量子计算的路"。路缩短了多少没人能答，但两条腿走路，总比单脚跳体面。