AlphaProof Nexus ── Lean で検証しながら未解決問題を解く AI エージェント

AlphaProof Nexus は、Google DeepMind の研究者21人が2026年5月21日に arXiv で発表した、数学の未解決問題に挑む AI エージェントの枠組みである。大規模言語モデルが証明を書き、証明支援系 Lean のコンパイラがそれを一段ずつ検査する。この往復を繰り返すことで、論文によれば、形式化された未解決のエルデシュ問題353問のうち9問を、1問あたり数百ドルの推論コストで自律的に解いた。うち2問は1970年に出されてから56年間未解決だった。査読を経た版は2026年10月8日に Science に掲載されている。

前日の5月20日には OpenAI が 単位距離予想の反証を発表しており、2日続けて AI 企業がエルデシュ問題での成果を競う形になった。両者の違いは方法にある。OpenAI の結果は自然言語の証明を人間が検証したものだったが、AlphaProof Nexus は、Lean が正しいと認めた証明だけを成果とする。

仕組み ── 書く AI と、検査する Lean

論文は、言語モデルの数学能力は高まっているが、信頼性の低さが研究での有用性を制限していると書き出す。その対策が、Lean のような形式言語で証明を書かせ、コンパイラにすべての論理の段階を自動で検証させる方法である。

利用者は、目標の定理と、証明の代わりに「sorry」と書いた Lean のファイルを渡す。エージェントは補題や定義を書き足し、Lean がエラーを返せばそれを手がかりに直す。全機能のエージェントは、AlphaProof（2024年）を、部分的な目標を片づける道具として呼び出せる。

成果

論文が例に挙げる第12問は、Erdős と Sárközy が1970年に出した、整数列の割り切れ方に関する問題で、複数の数学者が部分的な結果を出していた。エージェントは、急速に増える数列を使って「ブロック」を積み重ねる構成で答えた。第125問は、3進法で0と1だけを使う数の集合と、4進法で同様の集合の和について、1996年から未解決だった問いである。

最も単純なエージェントでも解けた

研究チームは後から、4種類のエージェントを、全機能版が解いた9問で比べた。驚くべきことに、と論文は書く。基本のエージェント (A) も9問すべてを解き、ただ難しい問題ではコストが高かった。論文はこの結果を、言語モデルが強くなるにつれ、特化して訓練したシステムから単純なエージェントの反復へと流れが移りつつあることを示すものだと解釈している。

失敗の分析も率直だった。エージェントは、問題の核心をそのまま言い換えた補題に「sorry」を置いて難しさを先送りすることが多く、プロンプトで禁じても止まらなかった。また、いくつかの問題では、文献で確立済みだとエージェントが主張した補題が、人が確かめると幻覚だった。論文は、こうした失敗こそ端から端までの形式検証の価値を示すと書いている。

評価 ── 2.5%をどう読むか

The Decoder は、353問中9問、約2.5%という数字は、AI がエルデシュ問題を解ける割合は1〜2%程度だという Terence Tao の推計に近いと指摘した。エルデシュ問題の大半は依然として手が届かず、成果は組合せ論や数論などに偏っている。対象の353問も、erdosproblems.com の未解決問題（2026年8月時点で652問）のうち、Lean で形式化済みのものに限られる。GitHub で公開された結果は成功例だけだが、試みた問題の一覧も添えられており、成功率を外から確かめられる。

Quanta Magazine は、Erdős がかつて自腹の懸賞金を付けた問題が、いまや解くのに要したトークンの値段、つまり1問あたりのコストで語られるようになったと書いている。AlphaProof Nexus の論文は、まさにそのコストを主要な指標の一つとして示した。

誰にとって何が変わったか

形式検証付きの AI は、検証の負担を人から機械へ移す。Lean の証明は誰でも手元で検算できる。人が読み通さなければ正しさが分からないという、自然言語による AI の証明の弱点に対する一つの答えである。一方で、形式証明があっても人間が中身を理解していない状態が生まれる。2026年7月、エルデシュ問題の共同体は、Lean の形式証明はあるが人が消化していない問題を「open (Lean)」と分類し始めた。この論争は エルデシュ問題と AI（2026年） で扱っている。

論文はまた、このエージェントが組合せ論、最適化、グラフ理論、代数幾何、量子光学の研究で使われ始めていると書く。証明を探す道具が数学者の日常の研究環境に入り込むことは、四色定理（1976年）や Flyspeck（2014年）以来の計算機と証明の歴史の新しい段階である。流れは AI と数学の年表 にある。