PSI：AIシステムがアーロンソン・アンバイニス予想のLean証明を発見

Physical Superintelligence（PSI）は2026年11月6日、非公開のAnthropicモデルのインスタンスを活用した社内探索システムが、2008年以来未解決であったアーロンソン・アンバイニス予想の証明を発見したと発表した。同研究所によると、実行3日目に完全な証明がLeanに受理され、その後に2回の改良が行われたという。論文草稿とLean 4形式化コードは公開されている。

予想の概要

Scott AaronsonとAndris Ambainisは、量子コンピュータがランダムな文字列に対するYes/Noの問いに対し、古典コンピュータよりも指数関数的に少ないクエリ数で答えを出せるのかという問いを提起した。ショアのアルゴリズムをはじめとする目覚ましい高速化の大半は、入力に存在する希少な構造に依存している。純粋数学の命題である彼らの予想が真であれば、そうした構造が存在しない場合、古典計算のオーバーヘッドは量子クエリ数に対して高々多項式オーダにとどまることになる。

具体的には、T回のクエリ後、量子アルゴリズムが「Yes」と答える確率は[0, 1]の値をとる高々2T次の多項式となる。本予想は、このような多項式が十分な変動幅を持つ場合、常に十分に大きな影響度（インフルエンス）を持つ変数が少なくとも1つ存在すると主張する。これにより、古典コンピュータはごく少数のビットを調べるだけでその予測を模倣できる。

PSIの公開内容

研究ページとGitHubリポジトリでは、LovettとZhangの骨子を踏襲し、彼らが未解決のまま残していた不等式を置き換えることで構築された証明が説明されている。READMEによると、Leanコードはプレースホルダーや追加の公理を用いない4つの定理からなり、Leanカーネルの2つの実装によって再検証されている（バージョン4.33.0 / Mathlib v4.33.0、Apache 2.0ライセンス）。David Turtureanが研究を主導し、Jim Halversonが証明を監査、Phiala Shanahanが形式化をレビューした。

2026年8月には、スタンフォード大学の4人の研究者（Blanc、Docter、Strassle、Tan）がすでに特殊なケースを解決していた。PSIによると、彼らは現在この完全な証明を精読中であり、より簡潔な解説を準備しているという。PSIの発表には彼らによる称賛のコメントも掲載されている。

留意すべき限界事項

リポジトリでは、Leanコード内のPrintedConjectureという記述が印刷物として発表された元の予想と厳密に一致しているかどうかの確認は読者に委ねられている。また、改良された定理の1つは、本コード内では形式化されていないAgarwalとBen-Davidの仮定に依存している。自然言語の論文自体は機械検証されていない。さらに、Anthropicのモデルは名前も公開されておらず非公開であるため、結果の精査は可能でも発見プロセスの再現はできない。本稿執筆時点で、AaronsonやAmbainisによる公開の反応は確認されていない。