アーロンソン＝アンバイニス予想：AIが18年未解決の量子パズルを3日で証明

11月6日、Physical Superintelligence（PSI）という小さな会社が、10年前ならSFのように聞こえたであろう発表をした。非公開のAnthropicモデルを走らせるAI研究システムが、2008年以来未解決だった量子計算量理論の中心的な未解決問題、アーロンソン＝アンバイニス予想を証明したというのだ。システムは実行3日目には完全な証明を得ていた。論理の各ステップを機械で検証する証明支援系Leanがそれを受け入れた。PSIはその後、システムに関連問題に取り組ませ、結果を2度改良し、論文と公開のLean形式化を発表した。誰でもその仕事を再検証できる。

なぜこれが重要なのかを理解するには、量子コンピュータが実際に何を得意とするかから始めよう。1994年、ピーター・ショアは大きな数を既知の古典的手法よりはるかに速く因数分解する量子アルゴリズムを見つけた。しかしショアの高速化は稀な恵みに依存している。問題が繰り返しパターンを隠し持っており、量子コンピュータがその繰り返しの頻度を見つけるのだ。知られている劇的な量子高速化のほとんどは同じ仕組みで動いている。構造を利用するのである。

スコット・アーロンソンとアンドリス・アンバイニスは、不快な問いを投げかけた。そうした構造をほとんど決して持たないランダムな入力についてはどうなのか。量子コンピュータは、ランダムな文字列についてのイエス・ノー問題を、通常のコンピュータより指数関数的に少ないビットの読み取り回数で答えられるのか。彼らは多項式についての予想——純粋数学——を立て、それが真なら答えはノーであることを示した。ランダムな入力に対して、量子コンピュータはせいぜい多項式倍速いだけなのだ。この予想は量子計算量理論の中心的な未解決問題の一つとなり、2026年8月にはスタンフォードのグループがその特殊な場合——入力を固定回数の並列ラウンドで読む量子アルゴリズム——を証明した。

PSIの証明は、シャチャール・ロベットとジアポン・チャンの計画に従い、彼らの計画で予想として残されていた一つの不等式を、論文中で証明された新しい不等式に置き換えたもので、デイヴィッド・ライマーのバタフライ補題に基づくペアリング論法と、他のいくつかのグループの結果を用いている。関わった人間、PSIのデイヴィッド・タートゥリアンは、研究システムを構築し、問題を定め、実行し、論文の正確性に責任を負っている。アドバイザーのジム・ハルヴァーソンが証明を監査した。特殊な場合を証明したスタンフォードのグループは完全な証明を読み、コメントを送り、専門家向けのより短い解説を執筆中だ。これまでの彼らの評価は「これは巨大な成果だ」というものだ。

これがこのニュースの正しい読み方だ。戴冠としてではなく、検証可能な成果物を伴った主張として。Leanの受け入れは高いハードルだ。機械が論証のすべてのステップを検証したのである。Leanが検証できないのは、形式化された命題が数学者の本当に関心のある命題であるかどうか、あるいは形式化の過程で隠れた仮定が紛れ込んでいないかどうかだ。それは人間の専門家の仕事であり、まだ終わっていない。査読は行われていない。証明を見つけたモデルは公開されていないので、誰も発見の過程そのものを再実行できない。生み出されたものを調べることしかできないのだ。

そして、この発表が飛び込んだその週こそが、本当の物語だ。PSIの証明は孤立した出来事ではない。10月、OpenAIはAIが書いた722編の数学原稿を公開した。その中には擬リーマン予想、ユニークゲーム予想、そしてある特殊な形状の族に対するホッジ予想の証明の主張が含まれている。9月には『数学季刊』の論文が、AIシステムがk微分に関する条件付きの結果を無条件の定理に変える鍵となるアイデアを見つけ、重要な補題がLeanで形式的に証明されたと報告した。Axiomは約7,500ページのStacks Project——約1,600万行——を形式化し、代数幾何学の膨大な成果を機械で検証可能にした。パターンはもはや紛れもない。AIが提案し、Leanが裁く。ボトルネックは証明の発見から証明の検証へと移り、検証のペースを決めているのは依然として人間だ。

私が注目しているのはまさにこの変化だ。スタンフォードの解説がきれいに着地し、他のグループが欠陥を見つけなければ、アーロンソン＝アンバイニス予想の証明は、1か月以内に専門家の精査を生き延びた2つ目の主要なAI主張の成果となる。問いは、AIが最先端の数学ができるかどうかではなく、検証のパイプラインがどれだけ速くついていけるかになる。私の予測はこうだ。2027年12月31日までに、この証明は独立した数学者によって公開で確認される。スタンフォードグループの解説、査読付き学術誌への掲載、あるいはそれに相当する公開の専門家確認を通じて、証明に実質的な欠陥が見つからないまま。確率は65%とする。機械的なハードルはすでにクリアされ、適切な専門家がすでに関与している。しかし人間の確認は形式的な手続きではなく、定義の1つのずれが、Leanで検証された証明をいまも崩しかねないからだ。