初创公司称用未发布Anthropic模型破解量子猜想

专注物理学研究的 AI 初创公司 Physical Superintelligence（PSI）宣布，其研发系统利用未公开的 Anthropic 模型实例，成功证明了自 2008 年悬而未决的量子复杂度难题——Aaronson-Ambainis 猜想。

PSI 表示，系统在其自有基础设施上运行到第三天便生成了完整证明，并顺利通过了交互式定理证明器 Lean 的形式化验证。尽管该成果尚未通过学术期刊的同行评审，属于公司单方声明，但相关论文和经过机器验证的代码均已在开源社区公开，供外部学者检验。

证明的核心结论

Aaronson-Ambainis 猜想的核心在于探讨：面对完全随机、缺乏 Shor 质因数分解算法所依赖的隐藏模式的输入时，量子计算机是否能比经典计算机实现指数级加速。Aaronson 与 Ambainis 此前指出，如果关于有界低阶多项式的命题成立，那么量子算法在处理随机输入时的加速上限仅为多项式级别。

PSI 将这一结论概括为：“除非输入字符串具备极其罕见的特定模式，否则量子计算机无法节省指数级的查询次数。”该定理主要限制了算法读取输入的查询次数，而非总计算时间。

在推导过程中，系统最初给出了一个相对较弱的界。随后 PSI 让系统针对相关开放问题继续推演，先后两次优化了结论，最终版本被 Lean 完整采纳。该论证路线遵循了学者 Shachar Lovett 和 Jiapeng Zhang 的整体框架，通过行列式配对输入设置，成功证明了一个原本作为猜想留存的不等式。

人工校验与同行反馈

PSI 团队成员 David Turturean 主导搭建并运行了该系统，引导模型撰写论文草稿并对整体正确性负责。顾问 Jim Halverson 与 Phiala Shanahan 参与了证明审查并对形式化过程提供了建议。

项目 GitHub 仓库说明显示，整个证明、论文文本及形式化代码均由 AI 模型生成。Lean 代码中不包含任何未证明的占位符或额外添加的公理，且已由两个独立的内核实现完成交叉复核。读者和研究人员目前主要需核对形式化陈述是否与原始数学猜想完全等价。

斯坦福大学研究人员 Guy Blanc、Jordan Docter、Carmen Strassle 和 Li-Yang Tan 曾在今年 8 月解决了该猜想的一个特例。他们在研读完整证明后，在 PSI 发布的声明中评价其为“极具分量的重大突破”，“所有要素以一种近乎神奇的方式融会贯通”。

关键细节仍待揭晓

目前 PSI 尚未披露其调用的具体是哪一款 Anthropic 模型，Anthropic 方面亦未对此置评。此前，OpenAI 曾于 9 月宣称解决了一项涉及 Navier-Stokes 方程的问题。一系列由前沿大模型主导的数学突破，正持续引发学界关于 AI 对数学家职业前景影响的热议。