18年未解決の量子計算の予想を、AIが3日で証明した。PSIが未公開のAnthropicモデルで「Aaronson-Ambainis予想」を解いたと発表、Leanの機械検証つき

まず初めに

AIが数学の難問を解いた、という触れ込みは、この数年でもう何度も見た。たいていは「解いた気がする」の段階で止まる。今回はいつもと毛色が違う。証明を書いたのがAIでも、検算をしたのは人間ではなく、証明の一歩一歩を機械的に検査するLeanである。作文の上手さではなく、検算に耐えたかどうかが物差しになる。AIの「自信」とは最も相性の悪い土俵で勝負した、という点が今回の肝だ。

※個人の感想です

予想の中身――量子コンピュータは「何でも速い」わけではない

Aaronson-Ambainis予想は、Scott AaronsonとAndris Ambainisが2008年に立てた、量子コンピュータの速さの限界に関する予想です。

Shorのアルゴリズム（1994年）が大きな数の素因数分解を劇的に速くできたのは、入力に「繰り返し」という隠れた構造（パターン）があったからです。では、そうした構造を持たないランダムな入力に対してはどうなのか。AaronsonとAmbainisは、もし自分たちの多項式に関する予想が正しければ、量子コンピュータはランダムな入力では通常のコンピュータより指数的には速くなれない（せいぜい多項式的な差にとどまる）ことを示していました。つまりこの予想は、「量子の指数的な速さには構造が要る」という主張の数学的な裏付けにあたります。

PSIの発表によると、今回の証明で得られた bound（影響度の大きさの下限）は、影響度が少なくとも定数 c=815/(125π⁴)（約0.0025）× 分散の5/2乗 ÷ 次数の6乗 以上になる、という形です。一般の多項式に対する従来の下限は、次数に対して指数的に小さくなるものが最良だったとPSIは説明しています。

証明はどう作られ、どう確かめられたのか

PSIによると、証明の大枠はShachar LovettとJiapeng Zhangが用意した計画（分数証書に基づく方針）に沿っています。2人は計画の中の1つの不等式を未証明のまま残していました。今回の証明は、その予想されていた不等式を、行列式を使って設定同士を対応付ける新しい不等式に置き換えて証明した、という構成です。David Reimerの「Butterfly Lemma」などが部品として使われています。

検証の形が今回の特徴です。PSIは論文（人間が読む証明文）と、Lean 4による形式化（機械が検査できる形の証明）の両方を公開リポジトリで公開しています。同社の説明と二次資料によると、形式化には証明の穴（placeholder）や追加の公理は含まれておらず、宣言はLeanのカーネルと、独立実装のチェッカー（lean4lean）でも再検査されました。

ただし、限界も明記されています。第一に、Leanが受理したのは「Leanで書かれた文」の証明であり、その文がAaronsonとAmbainisの元の予想と本当に一致しているかは、人間が読み比べて確認する必要があります。第二に、人間向けの論文本文そのものは機械検証の対象外です。第三に、査読は未了です。PSIは「予想は定理になった」と宣言していますが、数学の世界でそれが確定するのは、専門家の確認を経てからです。

前段階の成果として、2026年8月にはStanford大学のGuy Blanc、Jordan Docter、Carmen Strassle、Li-Yang Tanが、並列に読む回数が固定された量子アルゴリズムという特殊ケースで予想の予測を証明していました。PSIによると、この4人は今回の完全な証明を読んでコメントを寄せ、専門家向けの短い解説を執筆中だということです。

誰が何をしたのか

PSIの発表では、技術スタッフのDavid Turtureanが主担当として明記されています。研究システムの開発、問題の選定と実行、モデルに論文の初稿をまとめさせる作業、初稿のレビューまでを行い、論文の正しさに責任を持つとされています。Jim Halversonが証明を監査し、Phiala ShanahanがLean形式化にコメントしました。使われたAnthropicのモデルが具体的にどれかは、PSIは公表していません。

同じ週には、Claudeの長期記憶の仕組みをAnthropic自身が解説した研究記事も出ています。未公開モデルの「研究する力」と、公開側の「覚える力の設計」が、同じ週に並んで見える形になりました。

IT Postの見方

IT Postでは、今回の本質は「AIが天才になった」ではなく、「AIの成果を人間が信用できる形に仕上げる手順が、数学では既に存在した」という点にあると考えます。Leanという検算機がある分野では、AIの主張は「信じる／信じない」ではなく「通った／通らない」で判定できます。証明の探索はAIの計算量勝負にでき、検証は機械に任せられる。この分担が成立する分野から順に、AIの研究成果は「発表」から「検証可能な成果物」に変わっていくはずです。

ただし、検算機が守ってくれるのは「文から結論までの道筋」だけである。

出発点の文が元の問題を正しく写しているか、という最も人間的な確認は残ります。ここを飛ばして「18年の難問が解けた」とだけ消費するのは早計です。Stanfordの4人のような、その予想で実際に仕事をしてきた専門家が読み始めた、という事実の方が、現時点ではよほど重い材料です。

今後どうなりそうか

今後の確認点は、専門家による定式化の一致確認と査読の行方、短い解説版の公開、そして同じ研究システムが関連する未解決問題でどこまで再現できるかです。使われたモデルが未公開である以上、他者が同じ条件で追試することは現時点ではできません。

IT Postでは、新しい公式情報が確認できれば続報として整理します。