PSI（Physical Superintelligence）团队利用 Anthropic 未公开 AI 模型，仅用三天就完成了悬置十余年的阿伦森 - 安拜尼斯猜想的形式化证明，并且依靠 Lean 4 证明助手完成机器核验，这项成果直接回答了量子计算什么时候才能拿到指数级加速，是量子计算基础复杂度理论很关键的进展，不过目前论文还没有走完同行评审流程，结论还需要学术界进一步核验确认。这个猜想在 2008 年提出，核心讨论低次多项式的变量影响力，它关系到量子优越性的边界：如果猜想成立，那么随机输入场景下量子计算机最多只有多项式加速，想要拿到大家期待的指数级提速，任务本身必须带有特殊的结构约束，不是随便一个问题交给量子机就能飞快跑完，之前很多数学家尝试手动推导都卡在中间步骤，而大模型擅长在形式化系统里试引理、找隐藏对称结构，刚好补上这类数学证明的短板。整套流程是先由研究人员把猜想翻译成 Lean 4 里严谨的形式化命题，搭建好量子信息相关的形式化库，交给 AI 模型去寻找引理和推导路径，AI 输出证明片段之后交给 Lean 自动校验，出错就反馈回去迭代修改，循环往复直到整套证明全部通过机器检查；完成证明之后，团队把完整 Lean 源码开源出来，任何人都可以本地重新运行核验。这个成果不代表 AI 直接独立搞懂量子理论，而是 AI 作为数学家的辅助工具，用来探索复杂数学证明，未来这类人机协作模式会更多用到复杂度理论、量子算法证明这类硬核科研里，但 AI 产出的证明思路依然离不开人类搭建框架、判断命题是否贴合原始猜想。
阿伦森 - 安拜尼斯猜想核心信息
| 项目 | 说明 |
|---|---|
| 猜想名称 | 阿伦森 - 安拜尼斯猜想（Scott–Andris 猜想） |
| 提出时间 | 2008 年 |
| 研究方向 | 布尔函数、低次多项式、量子计算复杂度边界 |
| 核心结论 | 低次有界多项式，一定存在影响力不可忽略的变量 |
| 量子层面意义 | 随机输入下量子算法无法稳定拿到指数加速，指数加速依赖任务自带特殊结构 |
AI 辅助证明完整流程
- 人类科研人员梳理猜想原文，把自然语言的数学命题转化为 Lean 4 形式化描述，搭建配套的量子信息形式库
- 接入 Anthropic 的 AI 模型，给模型提供形式化定义、已知引理，让 AI 尝试构造证明链条、寻找中间辅助定理
- AI 输出 Lean 代码形式的证明片段，提交 Lean 证明助手自动检查每一步逻辑推导
- Lean 报错就把错误信息回传给 AI，让 AI 调整引理、换证明路径，反复迭代
- 全部代码无报错之后，开源整套证明仓库，支持所有人本地复现、审计
成果价值与局限
✅ 价值
- 明确划定量子加速边界，帮研究者判断哪些问题有潜力实现量子优越性
- 验证 “大模型 + 交互式定理证明器” 这套范式可以攻克多年悬而未决的数学猜想
- 开源 Lean 源码，整个证明过程可复现、可机器校验，降低后续同行核验成本
❌ 局限
- 尚未经过正式同行评审，学界还在对证明细节、形式化命题和原始猜想的等价性进行讨论
- AI 没有独立提出猜想，只能在人类给定形式化目标后寻找证明路径
- Lean 只能检查形式推导逻辑自洽，不能自动保证形式化翻译没有偏离原本的数学问题
【相关 FAQ】
问题 1：PSI 使用 AI 模型证明的这个量子计算猜想，是不是意味着 AI 可以独立研究量子计算理论？
回答 1：不是，PSI 是依靠 AI 模型辅助完成阿伦森 - 安拜尼斯量子计算猜想的证明，整个研究框架、命题翻译、方向判断都是人类科学家完成，AI 只是用来探索证明步骤，不能独立做量子理论研究。
问题 2：PSI 借助 AI 模型证明的阿伦森 - 安拜尼斯量子计算猜想，对量子计算机实际开发有什么影响？
回答 2：PSI 借助 AI 模型证明的这个量子计算猜想，帮开发者理清量子加速的前提条件，说明量子计算机不是对所有任务都能指数级提速，做算法设计的时候需要优先挑选带有特殊结构的问题，不要盲目期待全场景量子加速。
问题 3：PSI 这次 AI 模型辅助证明量子计算猜想，证明结果可信度怎么样？
回答 3：PSI 这次 AI 模型辅助证明量子计算猜想，证明代码已经通过 Lean 4 机器验证，并且开源可以复现，但是论文还没有同行评审，形式化版本和原始猜想是否完全等价，还需要数学、量子领域专家进一步核对。
问题 4：PSI 用来证明这个量子计算猜想的 AI 模型，是市面上公开的 Claude 版本吗？
回答 4：不是，PSI 用来辅助证明阿伦森 - 安拜尼斯量子计算猜想的是 Anthropic 未对外发布的内部 AI 模型，公开渠道无法获取这个模型。
【参考资料】
[2026-11-08]（Anthropic 未公开模型 “立功”，AI 助力攻克量子计算重大猜想）环球网科技
[2026-11-07]（A proof of the Scott-Andris conjecture，PSI 预印本公告）PSI 官网
[2026-11-07]（PSI 团队利用 AI+Lean4 完成 Scott–Andris 猜想证明）智源社区
[2026-08-24]（A Machine-Verified Proof of a Quantum-Optimization Conjecture）arXiv
【免责声明】
本文仅为 PSI 使用 AI 模型证明阿伦森 - 安拜尼斯量子计算猜想的科研进展科普，不代表最终定论；该成果目前未完成同行评审，结论、证明有效性有待学术界核验；AI 辅助定理证明仍属于前沿方向，机器核验不等于数学上的最终确认；相关观点、推论仅供学习参考，不构成学术定论。