Physical Superintelligence 称其 AI 证明了 Aaronson-Ambainis 猜想
公司研究页与公开 Lean 4 仓库：内部系统使用未公开 Anthropic 模型找到自 2008 年未解证明；Lean 在第三天接受；同行评议仍待进行。
为何重要
该猜想追问量子算法何时能在无结构输入上以指数优势胜过经典算法。PSI 称其系统在运行第三天产出 Lean 核验证明，并两度改进。形式化已公开且无占位，但仍需确认 Lean 陈述与印刷猜想一致，独立同行评议未完成。八月证明特例的斯坦福研究者在 PSI 页面被引述赞扬结果。需关注 Aaronson、Ambainis 与外部形式化团体的评估。
要点
- 自 2008 年未解（Aaronson–Ambainis）
- Lean 在运行第三天接受证明
- 使用未公开 Anthropic 模型（声称）
- 论文与 Lean 4 仓库公开
- 同行评议仍待进行