11月7日、madrobot.blogが「An unreleased Anthropic model solved an 18-year-old quantum computing problem, a startup says」と題した記事を公開した。物理学特化のAIスタートアップがAnthropicの未公開モデルを用いて18年来の数学的難問を証明したとする報告で、機械検証済みの完全な証明がすでにGitHubで公開されている。

18年越しの数学的未解決問題をAIが証明

物理学特化のAIスタートアップPhysical Superintelligence（PSI）が、Aaronson-Ambainis予想の証明に成功したと発表した。この予想は量子コンピューティングの核心的な問いに関わるもので、2008年から未解決のままだった。

PSIが使用したのは、Anthropicの未公開モデルを組み込んだ自社開発のリサーチシステムだ。モデル名は明かされていない。なお、このモデルはPSIが自社システムを通じて間接的にアクセスしたものであり、Anthropicが直接関与した研究成果ではない点に留意が必要だ。システムの実行を開始してから3日目に完全な証明が生成され、数学的証明の各ステップを機械的に検証するシステムLean（証明支援系）がそれを受理した。その後PSIはシステムを関連する未解決問題にも向け、途中で結果をさらに2度改善したという。

証明の論文とLeanによる機械検証済みの完全な証明はGitHubで公開されており、第三者による確認が可能な状態だ。なお、査読はまだ通っていない。

Aaronson-Ambainis予想とは何か

量子コンピュータは一部の問題（たとえばShorのアルゴリズムによる素因数分解）では古典コンピュータを劇的に上回るが、それは入力データに「量子機械が利用できる隠れた構造」がある場合に限られる。問題は、ランダムな入力に対しても量子コンピュータは指数的に速くなれるのか、というものだ。

Scott AaronsonとAndris Ambainis（現Anthropicアドバイザリーボードメンバー）はこれを純粋な数学命題——0から1の値をとる低次多項式に関する命題——に帰着させた。彼らの2008年の論文では、この予想が真ならば、量子コンピュータはランダムな入力に対して古典コンピュータより最大でも多項式的にしか速くなれない（指数的な優位性は生じない）ことを示している。

ここで注目されるのは、予想の共同提唱者であるAmbainis本人がAnthropicのアドバイザリーボードに名を連ねている点だ。今回の証明にAnthropicのモデルが用いられたという構図は、提唱者自身が関与する企業の技術によって自らの予想が解決されたという、やや特異な利益相反的文脈を持つ。Ambainis本人は記事公開時点でコメントを出していない。

PSIの証明は、Shachar LovettとJiapeng Zhangが描いた証明の骨格をベースにしており、彼らが未証明のままにしていた鍵となる不等式を新たに証明し、明示的な上界を与えた。

誰が何をやったか

GitHubのノートは役割分担を率直に記している。数学的命題の定式化、論文の初稿、Leanによる形式化は「AIモデルが生成した」。PSIの技術スタッフであるDavid Turtureanが研究システムを構築し、問題を選び、論文の執筆をモデルに指示し、ドラフトをレビューした上で論文の正確性に責任を持つ著者として記載されている。PSIアドバイザーのJim Halversonが証明を監査した。

つまりこの成果は「AIが独力で数学を解いた」という単純な話ではなく、AIを研究インフラとして組み込んだシステムを人間が設計・運用し、AIが生成した出力を人間が審査した共同作業の産物である。モデルが果たした役割の具体的な比重は公開情報からは判断できない。

スタンフォード大学の研究者4名（Guy Blanc、Jordan Docter、Carmen Strassle、Li-Yang Tan）は2025年8月に予想の特殊ケースを証明しており、PSIによるとその後PSIの証明を読み込んでコメントを送ってきているという。彼らはこのように述べている。

This is a huge result. It resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups.

— Guy Blanc, Jordan Docter, Carmen Strassle, Li-Yang Tan（スタンフォード大学）、PSIによる引用

過去に「証明」が撤回された経緯

この予想には前例がある。2019年、Nathan KellerとOhad Kleinが証明を発表し、Aaronson自身がブログで報告したが、数週間以内に欠陥が発見されて撤回された。

今回PSIの主張が一概に否定しにくい理由はLean証明の存在だ。リポジトリには「主要定理はプレースホルダも追加公理もなく証明されており、Leanカーネルの2つの独立した実装で再検証された」と記されている。

ただし、機械検証が確認できるのはあくまで「形式的な命題が正しく証明されていること」であり、その形式的命題がAaronsonとAmbainisが意図した予想と一致しているかどうかは専門家の目で判断する必要がある。PSIはその判断を容易にするため、Leanの数学ライブラリしかインポートしない短いファイルに命題を切り出している。AaronsonとAmbainis本人ともに記事公開時点ではコメントを出していない。

数学×AIの成果が相次ぐ背景

この発表は、AIが数学の難問を攻略する事例が連続して報告されるなかで出てきた。Microsoftの研究者はAIエージェントが31年未解決のKLS予想の証明を助けたと報告し、OpenAIとAnthropicは同日に複数の数学的成果を発表した。一方でOpenAIは発表翌日に722本のAI生成数学論文のうち3本を撤回している。量子回路の分野でもClaudeが既存の最高設計を上回る回路を出力したという報告がある。

今回の発表がもうひとつ示唆するのは、Anthropicの未公開モデルがすでに外部研究者の手に渡り、数学の最前線で稼働しているという事実だ。

詳細はAn unreleased Anthropic model solved an 18-year-old quantum computing problem, a startup saysを参照していただきたい。