这个题目涉及 Anthropic 未公开模型在量子计算理论上的成果，我先并行查三路：英文原始报道与论文、中文科技媒体的转述细节、以及这条猜想本身的学术背景。
原始报道、技术解释和这条猜想的历史都已经找到，包括 2019 年那次 “证明后被撤回” 的先例。以下是成稿。
标题：三天、一个未公开模型、一道悬了 18 年的题：Aaronson–Ambainis 猜想被 Lean 验完之后，还差哪几关
物理研究机构 Physical Superintelligence（PSI）在 11 月 7 日对外公布，他们用一套自建研究系统调用 Anthropic 一款尚未发布的模型，在运行第三天给出了量子计算领域悬置 18 年的阿伦森 — 安拜尼斯猜想的完整证明，随后又做了两轮改进，最终版本通过 Lean 4 证明助手的机械检验，论文与证明代码已公开。这个猜想 2008 年由 Scott Aaronson 与 Andris Ambainis 提出，问的是一件事：量子计算机在什么条件下才能获得远超经典计算机的加速。证明给出的答案是 —— 必须有 “结构”，没有结构就没有指数级加速。但它并不否定量子计算：Shor 算法分解大数之所以快，正是因为它吃到了题目里的周期结构，这类加速照样成立。真正需要被纠正的预期是另一件事：很多人把 “量子计算机能把所有答案并行试一遍” 当成万能钥匙，这道题恰恰证明那把钥匙不存在。同时要如实说明成果的验证状态：Lean 编译通过、两套独立内核重检、无占位符也无额外公理，斯坦福四位研究过该问题的学者已阅读并称 “重大成果”；但正式的同行评审、独立团队的完整复现都还没发生，60 页论文本身也没有经过机器检查。更值得放在心上的先例是：这道猜想 2019 年被宣布证明过，不到一个月就有人在其中一个引理里找出致命漏洞，论文被撤回。所以对这则消息最合适的定位是 “重大进展、待验证”，而不是 “量子计算被 AI 定论了”。
凤凰网一、先把事件还原成可核对的版本
| 项目 | 内容 |
|---|---|
| 主体 | PSI（Physical Superintelligence），2026 年 9 月才公开亮相的 AI 物理研究机构 |
| 工具 | 一款 Anthropic 尚未发布的模型，具体型号未披露；Anthropic 未回应置评请求 |
| 系统 | 由 PSI 技术人员 David Turturean 搭建，跑在实验室自有基础设施上 |
| 耗时 | 第 3 天给出完整证明，之后又改进两轮 |
| 验证 | Lean 4 编译通过；用两套独立实现的 Lean 内核重检；无 “先跳过回头再证” 的占位符，未引入额外公理 |
| 公开 | 论文与 Lean 证明代码已公开，地址可查 |
| 外部反馈 | 斯坦福 Guy Blanc、Jordan Docter、Carmen Strassle、Li-Yang Tan 四人已阅读并提供意见，称 “重大成果”，并准备为专业人士写更简洁的说明 |
| 尚未完成 | 期刊同行评审、外部团队独立复现；State of Proof 表示尚未独立重现检验 |
这里有一个容易被报道略过的分工事实：数学陈述、论文初稿、形式化证明都由模型生成，但问题由人选定、系统由人搭建，Turturean 本人审阅论文并对正确性负责。把它写成 “AI 独立发现了定理” 是不准确的。
二、这道题到底在问什么
不看公式也能理解。想象一排藏在帘子后面的开关，每个开关对应输入里的 0 或 1。题目是一道是非题，比如 “开着的开关是不是超过一半”，机器只能回答 “是” 或 “否”。想知道答案，就得掀帘子看开关，比的不是算得多快，而是看得多少次。
经典计算机一次只能看一个开关。量子计算机靠叠加态，一次能同时 “看到” 多个，但看到的信息是混在一起的，没法一次全看清。于是问题变成：量子机能不能靠这种并行观察，把需要的查看次数压到指数级地少？
Aaronson 和 Ambainis 的思路是把这件事翻译成一个关于 “影响力” 的命题：量子机回答 “是” 的概率像一个表盘，指针连着所有开关；某个开关状态一变，指针平均挪动的幅度就是它的 “影响力”。猜想说的是 —— 不管有多少个开关，只要指针不是纹丝不动，就一定有某个开关的影响力足够大。
这句话一旦成立，经典计算机就有了模拟的办法：先找一个影响力大的开关看，看完再找下一个，直到剩下的开关怎么变指针都不动为止。每一步都有值得看的目标，指针可晃动的余地越来越小，于是经典机需要的查看次数最多是量子机次数的某个固定次方，不会指数爆炸。
| 层级 | 命题形态 | 说明 |
|---|---|---|
| 底层 | 有界低次多项式必有影响力大的变量 | 纯数学陈述，与量子无关，可用离散傅里叶分析工具 |
| 中层 | 阿伦森 — 安拜尼斯猜想 | 把模拟问题归约成上面的多项式命题 |
| 顶层 | 模拟猜想：t 次查询的量子算法，大多输入可被 poly (t) 次经典查询模拟 | 若成立，量子加速必须依赖结构 |
这解释了为什么这条结论在产业上有意义：它给 “量子计算擅长什么” 划了一条边。NP 完全问题长期看不到量子指数加速，密码学里却能看到，差别就在题目自不自带结构。
三、三天是怎么做到的，以及为什么不是 “三天从零开始”
媒体标题里的 “3 天” 很容易被误读成 “从零到证明”。实际路径更像一次有准备的冲刺。
| 环节 | 谁做的 | 关键点 |
|---|---|---|
| 形式化底座 | 人 | 基于一套已相当完备的 Lean 量子信息库，把 QAOA 类组件、伊辛链、Jordan-Wigner 变换等已知部分形式化 |
| 缩小缺口 | 人 | 把整个猜想归约成一条尚未解决的数学命题，交给模型 |
| 找证明 | AI | 在 Lean 中构造证明，自然语言推理与编译器反馈形成闭环，期间还用 Python 做数值预检，避免在明显为假的方向上耗时间 |
| 逐行验 | Lean | 编译通过即表示结论由假设与所设公理推出 |
| 判断 “题目有没有理解对” | 人 | 校对形式化命题是否忠实表达原猜想，这是唯一必须人来把关的环节 |
技术上的关键突破点很具体：2023 年 Shachar Lovett 与 Jiapeng Zhang 提出过一套证明方案，卡在一个他们自己也没能证明出来的不等式上；PSI 的系统换用了一个新的不等式，并把它证出来，绕过了这道坎。论文摘要还提到，模型发现并利用了问题中一个此前未被察觉的动力学对称性，从相邻领域借来工具，把一个困难的存在性问题转成了显式构造。
这一点比 “3 天” 更值得记住：AI 没有凭空造出新数学，它是从已有工作里找到一个此前没被走通的组合方式。这和 Anthropic 8 月在黎曼 zeta 函数上的那次结果逻辑一致 —— 那次也是把几十年来不同数学家的方法重新排列，把 “至少多少比例零点在临界线上” 的可证下界从 41.6% 推到 67.2%。
四、这个结论对量子计算意味着什么，不意味着什么
| 它确实说明的 | 它并不说明的 |
|---|---|
| 无结构问题上，量子机最多拿到多项式级加速 | 量子计算失去价值 —— 有结构的问题照旧能吃指数加速 |
| 量子优势的成立依赖于问题或输入自带规律 | 所有量子算法都被同一把尺子量死 ——Shor、Simon 这类靠隐藏子群的算法不受影响 |
| “并行试遍所有答案” 是误解 | 现有的量子硬件路线错了 |
| 评价量子算法要看查询复杂度这个理论指标 | 现实设备的实际运行时间也受限 —— 报道明确提示，查询次数不能直接等同于总运行时间 |
对产业侧的实用含义有三条：
- 算法选型要更看重 “结构”。找隐藏周期、找代数结构、找可归约的对称性，这类方向的理论支撑更硬；泛泛地指望量子机硬解组合优化，期待要往下调。
- 硬件投入的叙事需要分层。容错、纠错、魔态培育这些工程进展是真实存在的（今年 10 月谷歌在 Willow 上把魔态培育的错误率降低约 40 倍、T 态逻辑保真度做到 99.99%），但它们解决的是 “能不能稳定算”，不是 “什么题值得算”。
- 投资与采购的尽调要多问一句：这个场景的结构在哪里。答不上来，理论上限就不高。
五、验证状态：已经过的关和还没过的关
| 关口 | 状态 | 说明 |
|---|---|---|
| Lean 编译 | 已过 | 证明由内核逐行检查，标准经典公理集，无占位符 |
| 双内核重检 | 已过 | 用两套独立实现的 Lean 内核各验一遍，降低实现层出错概率 |
| 代码与论文公开 | 已过 | 可被外部研究者取用 |
| 领域学者初读 | 已过 | 斯坦福四位学者阅读并给出正面评价 |
| Lean 命题与原猜想语义一致 | 待人工确认 | 形式化只保证 “从假设推出结论”，不保证 “假设写的就是原题” |
| 60 页论文本身 | 未机器检查 | 人读的文稿不在 Lean 覆盖范围内 |
| 期刊同行评审 | 未完成 | 目前仍是预印本状态 |
| 独立团队复现 | 未完成 | 追踪平台明确表示尚未独立重现 |
必须把 2019 年那次教训摆出来。那年 11 月，Nathan Keller 与 Ohad Klein 公布了一份证明预印本，Aaronson 还专门写博文给猜想标上 “2008–2019” 的时间段，等于认了。不到一个月，数学家 Paata Ivanishvili 在论文的一个引理里发现致命漏洞，随后两人撤回。一个引理，就足以让整座建筑倒掉 —— 这正是为什么 “Lean 通过” 值得重视，也是为什么它不等于 “数学界已承认”。
六、这不是孤例：2026 年正在形成一条 “AI 证明” 曲线
| 时间 | 主体 | 成果 | 验证方式 |
|---|---|---|---|
| 2026-06 | Anthropic（Claude Fable 5） | 证明 QAOA 在 “分歧环” 上的 FGG 猜想，近似比恰为 (2p+1)/(2p+2) | Lean 4 端到端验证，揭示隐藏动力学对称性 |
| 2026-08 | Anthropic（未发布研究版） | 黎曼 zeta 零点临界线比例下界 41.6%→67.2% | 内部数学家核查 + Lean + 两位外部专家审阅 |
| 2026-09 | Anthropic（Fable 5.1） | 数天内完成六粒子散射振幅九圈计算，刷新人类八圈纪录 | SLAC 与斯坦福教授独立验证，计算文件公开托管 |
| 2026-10 | Anthropic（内部模型） | 声称证伪指数时间假设 ETH | Lean 形式化，ETH 原始提出者参与组织审查 |
| 2026-10-26 | OpenAI | 一次性公布数学、计算机、物理三项突破 | 分梯度发布，邀外部专家牵头 |
| 2026-10-06 | OpenAI | 公开 722 份 AI 生成数学手稿，涉 372 个问题 | 随后撤回 3 篇、修订 14 篇 |
从这张表能看出一个正在发生的转变：发布策略从 “一次性全公开” 转向 “邀请原始提出者、诺奖得主牵头组队审查”。OpenAI 甚至把 AI 产物称作 “原始研究数据” 而非结论，并声明不索要学术署名。背后的现实是，AI 生成证明的速度已经超过人类消化证明的速度，瓶颈从 “找答案” 移到了 “验答案” 和 “讲清楚答案”。
七、以后看到这类新闻，用四条判据过一遍
- 有没有形式化，形式化到了什么程度。只有自然语言论文，和过了 Lean 内核，可信度不是一个量级。
- 形式化的命题是否忠实对应原猜想。这一步永远是人的责任，报道里如果不提，就要警惕。
- 有没有独立复现或同行评审。预印本 + 实验室自述，属于 “待验证”。
- 结论的适用边界写清了没有。是查询复杂度还是实际运行时间？是完整猜想还是低深度特例？是存在性还是连质量间隙一起解决？这三处最容易在传播中被放大。
顺带说一句边界：同一猜想在 “并行 / 低深度量子算法” 这个更窄的范围里，2026 年 8 月已有一篇论文给出解决，结论是 t 次查询、d 轮的量子算法可以被 t 的 O (d²) 次经典查询模拟；而 PSI 这次宣称的是完整版本。传播时如果把两者混为一谈，就会把 “部分解决” 说成 “早已解决” 或把 “完整证明” 说成 “只是重复”。
【相关 FAQ】
问题 1：Anthropic 未发布模型这次到底做了什么，3 天是怎么算的？
回答 1：PSI 用自建研究系统调用 Anthropic 未发布模型，让它在一个已形式化的 Lean 框架里补上最后一段证明。所谓 3 天，指系统运行到第三天给出完整证明，不含此前人类搭建形式化库、归约问题的时间；之后又做了两轮改进，最终版本通过 Lean 检验。模型型号 PSI 未披露，Anthropic 也未回应置评。
问题 2：阿伦森 — 安拜尼斯猜想被证明，是不是说明量子计算没那么有用？
回答 2：不是。这条猜想证明的是 “无结构问题上量子机拿不到指数级加速”，因此量子计算的价值更依赖问题自带的结构。Shor 算法分解大数之所以快，正是因为它利用了周期结构，这类加速不受影响。被否掉的是 “量子机能把所有答案并行试一遍” 的想象，而不是量子计算本身。
问题 3：Lean 验证通过了，是不是就等于数学界承认这个证明？
回答 3：不等于。Lean 只保证 “从写下的假设推出写下的结论”，不保证 “写下的假设忠实表达了原猜想”—— 后者仍需人工核对；60 页的人读论文不在机器检查范围内；此外还需要期刊同行评审与独立团队复现。目前的状态是：形式化通过、领域学者初读认可、正式评审未完成。
问题 4：为什么总提 2019 年那次撤回，跟这次有什么关系？
回答 4：因为它是这类成果最直接的参照。2019 年 11 月 Keller 与 Klein 公布过一份证明预印本，不到一个月就被 Paata Ivanishvili 在一个引理里找出致命漏洞，论文撤回。这说明一个引理出错就能让整体崩塌，也说明 “有人宣布证明” 和 “猜想真的被证明” 之间隔着很长一段验证路。
问题 5：Anthropic 未发布模型连续做出这类成果，说明 AI 已经能独立做数学研究了吗？
回答 5：还不到 “独立”。这几次的共同分工是：人选定问题、搭建形式化框架、把难题归约成一条可陈述的命题；AI 负责在框架内搜索并构造证明；Lean 负责逐行检验；人负责确认命题语义。AI 承担的是最耗人力的一段，但问题的选择与正确性的最终责任仍在人身上。
问题 6：这条量子计算猜想的证明，对做量子算法或投资的人有什么实际用处？
回答 6：最大的用处是给了筛选标准。评估一个 “量子能加速” 的场景时，先问它有什么结构 —— 隐藏周期、代数对称性、可归约的子群；答不上来，理论上限就不高。同时要把查询复杂度与真实运行时间分开看，别用理论上的查询次数去推硬件上的耗时。至于 3 天证明这件事本身，更适合当作 “AI 参与理论研究” 的样本，而不是量子硬件的利好或利空。
【参考资料】
[2026-11-08]（Anthropic 未发布模型参与研究，实验室称 3 天证明量子计算重要猜想（含 Lean 检验、斯坦福学者反馈、State of Proof 未独立复现））凤凰网科技・腾讯新闻
[2026-11-08]（Anthropic 未公开模型 “立功”，AI 助力攻克量子计算重大猜想（环球网科技综合报道，引 Business Insider））环球网
[2026-11-07]（Anthropic 神秘模型 “立功”，AI 帮助攻克量子计算领域重大难题）IT 之家・新浪科技
[2026-11-07]（刚刚，Anthropic 神秘模型出手！3 天攻克 18 年量子计算难题（含猜想通俗解释、2019 年撤回史、双内核重检））AI 信息 Gap・新浪科技
[2026-10-27]（OpenAI 掀翻计算机科学 30 年基石，还解决了挂谷猜想（含 722 篇手稿撤 3 修 14、分梯度发布策略））36 氪
[2026-10-27]（OpenAI 宣布斩获三项重大科学突破，涉及千禧年难题（含陶哲轩 “有毒废料” 批评））界面新闻
[2026-09-29]（仅用数天时间 大模型 Claude 完成散射振幅九圈计算（独立验证与成本披露））科技日报・新华网
[2026-08-20]（Quantum Speedups Require Structure or Depth（同一猜想在低深度 / 并行算法范围的解决，t 次查询 d 轮可被 t^O (d²) 次经典查询模拟））arXiv 2608.19158
[2026-08-11]（Claude 挑战黎曼猜想 “失败”，却意外刷新 37 年数学纪录（临界线零点比例下界 41.6%→67.2%））机器之心・腾讯新闻
[2026-06-30]（A Machine-Verified Proof of a Quantum-Optimization Conjecture（Claude Fable 5 证明 FGG 猜想并经 Lean 4 验证））arXiv 2606.29687
【免责声明】
本文依据 Business Insider 报道的中文转述、PSI 公开的项目说明与论文，以及 arXiv 预印本整理，未直接获得 Anthropic 官方确认；所涉模型型号、系统细节均以 PSI 披露为准，Anthropic 未回应置评请求。该证明目前处于预印本状态，尚未完成期刊同行评审，也未见外部团队独立复现；Lean 编译通过仅表示结论由所设假设与公理推出，不代表形式化命题与原猜想在语义上完全等价，60 页论文本身亦未经机器检查。文中关于量子计算产业影响的判断属分析，不构成投资建议。AI 辅助科研成果的可靠性应以正式评审与独立复现为准，请勿据本文作出技术采购或投资决策。