PSI 宣称 AI 系统证明 18 年未解量子猜想，Lean 全程机检

winer666 · reddit · 2026-11-08

Physical Superintelligence（PSI）11 月 6 日宣布：其内部研究系统（运行某个未公开的 Anthropic 模型实例）在运行第三天给出了 Aaronson–Ambainis 猜想的完整证明。该猜想自 2008 年悬而未决，关乎量子计算在非结构化问题上能否相对经典计算机获得指数加速。
证明由 Lean 定理证明器接受：形式化包含 648 个机器检查的定理，无占位符、无附加公理，并通过 Lean kernel 与独立检查器 lean4lean 重放验证；系统随后还两次改进结果，每次都经 Lean 重新检查。论文与 Lean 4 形式化已公开。
注意事项：形式化命题是否与 Aaronson–Ambainis 原始猜想一致仍需人类数学家确认；文字版论文未经机器检查；背后的模型不公开，三天运行过程无法复现——只有最终证明可被验证。
若站得住脚，这是 AI 真正「做数学」而非仅辅助的标志性案例，但也引出问题：发现过程不可审查、只能验证最终证明，这会如何改变数学的做信任方式？

「模型」频道最新