PSI 实验室借助 Anthropic 未公开的内部模型和 Agent Harness 这套智能体调度系统，只用三天时间，完成了困扰学界长达 18 年的 Aaronson-Ambainis 猜想的证明，也就是大家口中的量子计算圣杯，整套证明还通过 Lean 证明助手的形式化校验，这也是 AI 智能体在量子信息理论领域里程碑式的成果。这个猜想是 2008 年由 Scott Aaronson 和 Andris Ambainis 提出，核心是划定量子计算机拿到指数级加速的边界，搞清楚量子优势到底在哪些条件下才成立，过去十几年无数顶尖数学家、量子方向研究者尝试推导，一直没能拿出完整严谨的证明；而 Agent Harness 不是简单调用大模型，它会自动拆分数学命题、迭代推导思路、自动生成形式化代码、把中间结果送进 Lean 校验，发现逻辑漏洞之后自动回头修正，不用科研人员全程盯着每一步推导，大幅压缩了漫长的试错周期；整个流程是研究人员定下目标，交给这套智能体系统自主循环推进，第三天输出首版完整证明，后续系统又迭代优化了两个版本，目前论文、形式化证明代码已经对外公开，不过成果还需要更多同行独立审查确认，猜想提出者 Ambainis 本人也对这次 AI 辅助证明给出了正面评价。
一、核心名词简单解释
- Aaronson-Ambainis 猜想：量子信息领域经典难题，用来回答量子计算机能不能随便对任意输入拿到指数加速，决定量子优势的理论上限。
- Agent Harness：一套智能体调度框架，负责给大模型分配科研子任务、串联工具、接收校验反馈、自动重试迭代，相当于驾驭模型做复杂数学推理的控制系统。
- Lean：交互式证明助手，可以逐行检查数学推导逻辑，排除人为疏漏，是数学领域公认的严谨校验工具。
- PSI（Physical Superintelligence）：主导本次研究的实验室，专门研究 AI 辅助物理、量子方向的前沿科研。
二、整套攻关流程清单
- 任务输入：科研人员把 Aaronson-Ambainis 猜想、已知前置引理、领域文献喂入 Agent Harness 系统，设定证明目标与 Lean 输出规范。
- 思路发散：Agent Harness 调度 Anthropic 内部模型，把大猜想拆成多个更小的引理、子命题，规划多条证明路线。
- 形式化生成：模型把推导思路翻译成 Lean 可识别的形式化代码，自动补齐推导细节。
- 自动校验：提交 Lean 跑验证，如果报错，Harness 捕获错误信息，再传给模型定位漏洞、修改证明。
- 迭代收敛：循环 “推导 - 编码 - 校验 - 修复”，系统在第三天产出第一份完整通过 Lean 校验的证明。
- 整理输出：自动整理论文叙述版本，研究者复核，对外公开论文与开源证明代码。
三、容易混淆的关键点对比
| 项目 | 本次事件说明 | 容易搞错的误区 |
|---|---|---|
| 模型身份 | Anthropic 未公开内部模型，暂未对外发布版本 | 不是公开版 Claude，官方没有公布具体型号 |
| Agent Harness 角色 | 任务调度、反馈闭环、工具串联框架 | 它本身不是大模型，是驾驭模型做科研的系统 |
| 成果性质 | 猜想的形式化证明，通过 Lean 验证 | 不等于已经完成全行业同行终审，仍待独立复现审查 |
| 研究结论 | 量子指数加速依赖问题本身特殊结构，随机输入很难拿到巨大优势 | 不是否定量子计算机，只是划定量子优势边界 |
四、这件事带来的影响
✅ 正向影响
- 证明 Agent Harness 架构适合高难度数学、量子理论类科研，能把几年量级的攻坚压缩到几天。
- 给量子计算领域提供理论边界参考，后续设计量子算法、量子硬件时可以避开不存在指数加速的场景。
- 给 AI for Science 提供一套可复用范式：智能体 + 大模型 + 形式化证明助手的闭环。
⚠️ 需要理性看待的地方
- Lean 通过只代表推导逻辑自洽，不等于学界立刻全盘接受，独立复现和同行评议是必不可少环节。
- Agent Harness 依然需要人类选定问题、把控方向，不能做到完全无目标自主发现重大难题。
- 该成果属于理论证明，不会立刻改变现在量子计算机硬件研发进度。
五、实操层面的启发
如果想要复刻这类 AI 数学科研流程，Agent Harness 是核心骨架，单纯丢给大模型 “直接证明猜想” 基本很难成功；一定要加上形式化校验工具做反馈，让智能体知道哪一步推导出错；复杂数学证明适合拆成子任务分批处理，不要一次性要求模型完成超长链路推理。
【相关 FAQ】
问题 1：本次攻破量子计算 Aaronson-Ambainis 猜想，Agent Harness 起到了什么样的作用？
回答 1：Agent Harness 是整套系统的调度中枢，负责拆分量子猜想的证明任务、调度 Anthropic 模型、把推导代码送入 Lean 校验、捕获报错并且驱动模型自动修改证明，正是这套闭环能力，才让它仅用三天完成量子计算 Aaronson-Ambainis 猜想的证明。
问题 2：三天被攻破的这个量子计算圣杯，是不是代表量子计算没有前景了？
回答 2：不是，这次借助 Agent Harness 证明的 Aaronson-Ambainis 猜想，只是说明量子指数级加速有前提条件，随机无特殊结构的任务很难拿到巨大优势，并没有否定量子计算在密码、模拟、优化等场景的价值。
问题 3：用来攻坚量子计算猜想的 Anthropic 模型和 Agent Harness，现在对外公开可用吗？
回答 3：本次使用的 Anthropic 模型属于内部未发布版本，没有开放调用；Agent Harness 是 PSI 实验室自研的科研调度系统，本次配套的证明代码已经公开，但完整的这套科研 Agent 流水线没有直接对外发布。
问题 4：Aaronson-Ambainis 猜想的证明通过 Lean 校验，是不是代表这个量子计算成果已经完全定论？
回答 4：Lean 校验只能确认证明内部逻辑自洽，依靠 Agent Harness 产出的这份 Aaronson-Ambainis 猜想证明，仍然等待量子信息、数学领域其他独立团队复现和同行评审。
【参考资料】
[2026-11-08]（PSI 称用 Anthropic 未公开模型 3 天证明量子计算重要猜想，成果尚待独立审查）凤凰网科技
[2026-11-07]（刚刚，Anthropic 神秘模型出手！3 天攻克 18 年量子计算难题）新浪科技
[2026-11-07]（A 社超强模型曝光！三天攻破量子计算圣杯，Agent Harness 立大功）新智元（今日头条转载）
[2026-08-17]（闭源 RSI 的严父来了：18 个 Agent 自主科研，Kimi K3 靠 Harness 逼近 Opus 5）量子位
【免责声明】
本文信息仅为前沿科技资讯整理，不代表学术最终定论；本次基于 Agent Harness 完成的 Aaronson-Ambainis 猜想证明，尚未完成完整独立同行评议，最终学术结论以后续正式期刊、学术会议发布版本为准；Agent Harness 与配套 Anthropic 内部模型暂未开放，不构成任何商用、二次复刻的落地承诺；AI 科研工具存在推理幻觉风险，形式化校验也无法替代领域专家的专业审核。