模型与验证
未公开的 Anthropic 模型，三天，一个 2008 年猜想有了完整证明
PSI 的 AI 研究系统在 run 第三天就有了 2008 年 Aaronson–Ambainis 猜想的完整证明，Lean 证明助手接受了最终版形式化；但审计者是 PSI 自己的员工，模型名称未公开，这个猜想十年前还有过一份被撤回的证明——“专家验证进行中”是这条公告的准确读法。
本文依据 PSI 研究公告页（页面标注 2026-11-06，本站 11 月 8 日读取）、Lean 形式化仓库（11 月 8 日 API 核对）与 Scott Aaronson 2019 年的猜想历史回顾（11 月 8 日读取）写成；媒体转述（IT之家转引 Business Insider，11 月 7 日）仅作时间线参照。PSI 是发布方自己的公告口径，不是独立评议结论；本站未验证证明、未运行模型、未逐行检查 Lean 代码。
三天，Lean 接受
11 月 6 日，研究组织 Physical Superintelligence（PSI）在其研究页公告：其 AI 研究系统产出了 2008 年开放问题——Aaronson–Ambainis 猜想——的完整证明，Lean 证明助手接受了系统的形式化。配套仓库当天建立（本站 11 月 8 日 API 核对：2026-11-06T03:19Z 创建、单次推送、Apache-2.0 许可、仓内含论文 PDF）。公告同时写明了参与系统的模型：「Instances of a non-public Anthropic model were used in the run」——一款未公开的 Anthropic 模型，没有名称、版本或规模。Anthropic 自己没有发布任何确认。
时间线在公告里写得很具体：run 的第三天，系统就「已有完整证明」，之后又改进了两次，Lean 接受了最终版本。人物分工同样写明：David Turturean 领导这项工作并对证明正确性负责；Jim Halverson 审计了证明；Phiala Shanahan 评论了 Lean 形式化。11 月 7 日，Business Insider 的报道与 IT之家的转述让「未公开的 Anthropic 模型」进入大众视野——转述里那句「PSI 具体使用了何种模型暂时不得而知」，正是这件事最准确的注脚。
这不是 Anthropic 模型第一次碰 Lean 数学。站内 9 月 9 日的文章记录过：Anthropic 用约相当于 Fable 5.1 的内部研究模型加多个 Agent，约 11 天把费马大定理——一个已有人类证明的定理——形式化进 Lean。9 月与 11 月的差别值得记住：9 月是把已有的证明搬进检查器；11 月这次，如果专家验证站得住，就是一个开放问题上的新证明。两类工作的难度与验证要求都不同，本站未验证证明、未运行模型，两类信息分开读。
来源与延伸阅读
- PSI：A proof of the Aaronson-Ambainis conjecture（研究公告页）发布方公告 · 页面标注 2026-11-06（本站 11-08 读取）全文读取：run 由未公开的 Anthropic 模型实例参与、公告口径第 3 天已有完整证明、之后两次改进且 Lean 接受最终版；David Turturean 领导并对证明正确性负责，Jim Halverson 审计证明，Phiala Shanahan 评论 Lean 形式化；2026 年 8 月证明过特例的 Stanford 小组（Blanc、Docter、Strassle、Tan）正在阅读完整证明并撰写更短的专家导论。定理写法：Infi(f) ≥ c·v^(5/2)/d⁶ ≥ (v/d)⁷，c = 815/(125π⁴) ≈ 0.0025。页面同时写明结果适用于随机输入上的布尔输出问题。审计者均为 PSI 员工，页面未声称任何独立同行评议或期刊接收。
- GitHub：physical-superintelligence/aaronson-ambainis（Lean 形式化与论文）机器可查形式化 · 11 月 8 日 API 核对仓库 2026-11-06T03:19:45Z 建立、03:19:52Z 推送（单次推送），Apache-2.0 许可，观察时 41 stars；citation_pdf_url 指向仓内 paper/aaronson_ambainis_paper.pdf。本站未检出仓库证明、未运行 Lean。
猜想说的是什么：量子加速需要结构
Aaronson–Ambainis 猜想 2008 年提出，说的是低次多项式的一个 influence 下界：取值在 [0,1] 的有界 d 次多项式 f，若方差为 v，则必有某个变量的 influence 至少是 (v/d) 的固定次幂。PSI 公告把常数写到了具体值：Infi(f) ≥ c·v^(5/2)/d⁶ ≥ (v/d)⁷，其中 c = 815/(125π⁴) ≈ 0.0025（公告原文口径）。它为什么重要：2011 年 Aaronson 与 Ambainis 合写《The Need for Structure in Quantum Speedups》，把一串「量子计算何时真能加速」的问题归约到这个猜想——若猜想成立，量子计算机对随机（无承诺结构）输入的加速至多是多项式级，Shor 那样的指数加速需要问题本身带结构。
这个猜想不是没人碰过。Aaronson 的 2019 年回顾记录了十年攻击：O'Donnell、Kindler，甚至 Terence Tao 都试过。2019 年 11 月，Nathan Keller 与 Ohad Klein 的预印本自称证明，Aaronson 读后曾称「great」；随后两位作者撤回了预印本——Lemma 5.3 有一个在当时看是致命的漏洞，由 Paata Ivanishvili 发现。撤回事件解释了这个领域读任何新声明时的默认姿势：先问形式化在哪、谁能复验，再谈结论。
离这次公告最近的一步是 2026 年 8 月：Stanford 的 Blanc、Docter、Strassle 与 Tan 证明了猜想的一个特例。PSI 公告写明，这个小组正在阅读完整证明，并在写一份更短的专家导论——进行中、尚未发表。换句话说，当前最接近这个问题的一线研究者还没有给出他们的读法，这是评估这条公告时最值得等的一件事。
来源与延伸阅读
- PSI：A proof of the Aaronson-Ambainis conjecture（研究公告页）发布方公告 · 页面标注 2026-11-06（本站 11-08 读取）全文读取：run 由未公开的 Anthropic 模型实例参与、公告口径第 3 天已有完整证明、之后两次改进且 Lean 接受最终版；David Turturean 领导并对证明正确性负责，Jim Halverson 审计证明，Phiala Shanahan 评论 Lean 形式化；2026 年 8 月证明过特例的 Stanford 小组（Blanc、Docter、Strassle、Tan）正在阅读完整证明并撰写更短的专家导论。定理写法：Infi(f) ≥ c·v^(5/2)/d⁶ ≥ (v/d)⁷，c = 815/(125π⁴) ≈ 0.0025。页面同时写明结果适用于随机输入上的布尔输出问题。审计者均为 PSI 员工，页面未声称任何独立同行评议或期刊接收。
- Scott Aaronson：The Aaronson-Ambainis Conjecture (2008-2019)（博客回顾）猜想命名人回顾 · 2019-11-17（含后续更新）· 本站 11-08 读取历史核对：Aaronson 约 1999 年起沿 Fortnow–Rogers 路径思考随机预言机问题；2008 年形成 influence 猜想；2011 年与 Ambainis 合写《The Need for Structure in Quantum Speedups》把一串量子加速问题归约到它；十年间 O'Donnell、Kindler、Tao 等人攻击过。2019 年 11 月 Keller–Klein 预印本自称证明，Aaronson 当月曾称「great」；置顶更新写明两人撤回预印本——Lemma 5.3 存在当时看是致命的漏洞，由 Paata Ivanishvili 发现。这是本篇读 PSI 公告时保留谨慎的依据。
验证链：机器查逻辑，人查方向
这条公告的可信度不在「AI 三天证明了一个难题」这句话里，而在验证链的每一层各查了什么。机器层：Lean 证明助手按形式规则逐步核查，Lean 接受意味着证明的每一步都能从公理推出、没有跳步——这一层是机器完成的，任何人都可以拿公开仓库复验，验证成本从「读完几百页证明」变成「跑一遍检查器」。人层：Turturean 对正确性负责、Halverson 审计、Shanahan 评论形式化——这一层查的是机器层查不了的东西：证明的方向是否有意义、形式化陈述是否对应原猜想。
费马形式化那次站内已经写过一个关键细节：Lean 只保证形式化内部一致，「形式陈述是否对应原问题」还需要单独核对——公理检查与 Mathlib 陈述比较承担其中一部分。这次同理：Lean 接受不是终点， PSI 页面也没有声称独立同行评议已经发生；写明的审计者都是 PSI 自己的员工。另一处缺口在模型：名称、版本、规模都未公开，AI 与人的贡献占比无法独立评估——「三天出证明」里有多少是模型能力、多少是 harness 与人的设计，目前是读不出来的。
还有一层边界值得单独写：本站未验证证明、未运行 Lean、未逐行检查仓库——本篇的全部事实依据是公告页、仓库元数据与 Aaronson 回顾。读者同样不需要亲自读懂证明才能跟进：等两个信号即可——Stanford 小组的专家导论，以及 Aaronson 与 Ambainis 本人的表态。这两个信号出现之前，「Lean 通过」的正确读法是「形式化内部一致且公开可查」，不是「数学界已确认」。
来源与延伸阅读
- PSI：A proof of the Aaronson-Ambainis conjecture（研究公告页）发布方公告 · 页面标注 2026-11-06（本站 11-08 读取）全文读取：run 由未公开的 Anthropic 模型实例参与、公告口径第 3 天已有完整证明、之后两次改进且 Lean 接受最终版；David Turturean 领导并对证明正确性负责，Jim Halverson 审计证明，Phiala Shanahan 评论 Lean 形式化；2026 年 8 月证明过特例的 Stanford 小组（Blanc、Docter、Strassle、Tan）正在阅读完整证明并撰写更短的专家导论。定理写法：Infi(f) ≥ c·v^(5/2)/d⁶ ≥ (v/d)⁷，c = 815/(125π⁴) ≈ 0.0025。页面同时写明结果适用于随机输入上的布尔输出问题。审计者均为 PSI 员工，页面未声称任何独立同行评议或期刊接收。
- GitHub：physical-superintelligence/aaronson-ambainis（Lean 形式化与论文）机器可查形式化 · 11 月 8 日 API 核对仓库 2026-11-06T03:19:45Z 建立、03:19:52Z 推送（单次推送），Apache-2.0 许可，观察时 41 stars；citation_pdf_url 指向仓内 paper/aaronson_ambainis_paper.pdf。本站未检出仓库证明、未运行 Lean。
怎样读这条公告：能力故事与验证故事分开
能力故事与验证故事分开读，是这条公告的正确姿势。能力故事：一款未公开的前沿模型，在研究 harness 里三天拿到开放问题的完整证明。验证故事：Lean 机器接受＋PSI 内部审计＋Stanford 小组阅读进行中＋独立评议未发生。两个故事现在都成立，但只有第一个适合传播，第二个才决定它最终在数学史上的位置——2019 年那份「great」的证明最后以撤回收场，说明第二个故事可以推翻第一个。
放到更大的图景里，这是「AI 解开放问题」这条线的第三种形态。腾讯 Hyra 1.0 用开源模型加自造工具处理加法组合学的开放问题（站内 Hy4 一文有记）；费马形式化是「已有人类证明＋AI 形式化」；这次 PSI 是「开放问题＋AI 新证明＋Lean 收口」。三种形态的验证要求依次升高， PSI 这次的验证链也是三者里最完整的一份公开记录——机器可查这一层做到了，人层还差独立评议。10 月 31 日的《谁对齐了谁》写过 AI 对专家判断的影响；这条公告把「模型作为研究参与者」又推进了一格，而验证链里的人层怎么补齐，正是接下来几个月值得盯的事。
对读者的三个可执行读法：一、想核对，Lean 仓公开（Apache-2.0），机器可查不等于人人能懂，但「有没有人复验过」从此有了明确去处；二、想跟进，等 Stanford 小组的专家导论与两位命名人的表态，任一出现都值得重读本篇；三、想理解这类公告，记住这次的结构——模型未公开、审计在内部、机器层已收口：能力上限与验证进度是两条独立的线，别让任何一条替另一条说话。
来源与延伸阅读
- PSI：A proof of the Aaronson-Ambainis conjecture（研究公告页）发布方公告 · 页面标注 2026-11-06（本站 11-08 读取）全文读取：run 由未公开的 Anthropic 模型实例参与、公告口径第 3 天已有完整证明、之后两次改进且 Lean 接受最终版；David Turturean 领导并对证明正确性负责，Jim Halverson 审计证明，Phiala Shanahan 评论 Lean 形式化；2026 年 8 月证明过特例的 Stanford 小组（Blanc、Docter、Strassle、Tan）正在阅读完整证明并撰写更短的专家导论。定理写法：Infi(f) ≥ c·v^(5/2)/d⁶ ≥ (v/d)⁷，c = 815/(125π⁴) ≈ 0.0025。页面同时写明结果适用于随机输入上的布尔输出问题。审计者均为 PSI 员工，页面未声称任何独立同行评议或期刊接收。
- Scott Aaronson：The Aaronson-Ambainis Conjecture (2008-2019)（博客回顾）猜想命名人回顾 · 2019-11-17（含后续更新）· 本站 11-08 读取历史核对：Aaronson 约 1999 年起沿 Fortnow–Rogers 路径思考随机预言机问题；2008 年形成 influence 猜想；2011 年与 Ambainis 合写《The Need for Structure in Quantum Speedups》把一串量子加速问题归约到它；十年间 O'Donnell、Kindler、Tao 等人攻击过。2019 年 11 月 Keller–Klein 预印本自称证明，Aaronson 当月曾称「great」；置顶更新写明两人撤回预印本——Lemma 5.3 存在当时看是致命的漏洞，由 Paata Ivanishvili 发现。这是本篇读 PSI 公告时保留谨慎的依据。
- Anthropic：Formalizing Fermat's Last Theorem（费马大定理形式化公告）官方公告 · 2026-09-04（本站 11-08 读取）费马形式化公告为站内 9 月 9 日《形式化证明在检查什么》一文的原始来源（站内文另记：Anthropic 用约相当于 Fable 5.1 的内部研究模型、多个 Agent 与 Prove2Me，约 11 天完成形式化；形式化还需核对形式陈述是否对应原问题，FinalCheck、公理检查与 Mathlib 陈述比较承担相关检查）。本篇与之对照：9 月是形式化已有证明，11 月 PSI 是开放问题上的新证明。