Anthropicの非公開AIモデルが、数学の難問として知られるリーマン予想の研究で前進を示した。一般的な証明には至っていないものの、リーマン予想が成り立つ範囲の下限を大きく引き上げたという。結果は社内の数学者2人が確認し、オープンソースの証明支援ツール「Lean」で形式化した。

米TechCrunchが11日（現地時間）に報じた。リーマン予想は150年以上にわたり未解決の代表的難問で、素数の分布に関わる。一般的な証明が示されれば、100万ドル（約1億5000万円）の懸賞金が授与されるが、これまで受賞者は出ていない。今回の成果も、その一般証明そのものではない。

それでも今回の結果は、AIはこうした難問にはまだ太刀打ちできないという見方に対し、実際の研究水準で一定の前進を生み得ることを示した事例といえる。

手法面でも注目を集めた。数学を専門に訓練してきたわけではないAnthropicの社員が、モデルに対してリーマン予想の証明を本格的に試みるよう指示し、その後は約1日半にわたり試行錯誤の多くをモデル側に委ねた。

その結果、モデルは650通りの異なるアイデアを試し、60のサブエージェントを動かしながら、計3100万トークンを消費した。

論文の脚注によると、60のサブエージェントのうち2体が中核となる数学的アイデアの創出を担った。さらに13体がそれらに追加の発想を与え、30体は新たなアイデアの創出を試みたものの成果は得られなかった。

残る13体は論証の正確性を検証し、最後の2体は論文の初稿作成に加わったという。

Anthropicは、こうした研究過程で得られた主張や論証をLeanで形式化した。内容を機械的に検証可能な形に落とし込んだことになる。

大規模言語モデルが数学研究で成果を示す流れは、ここにきて一段と鮮明になっている。今年に入ってからは、AIモデルがエルデシュ問題を複数解決したとされ、より高性能なモデルの登場とともに成果の水準も上がっている。

OpenAIも最近、内部モデル「Astra」が証明した主要な結果10件を公開した。Anthropicの別の研究では、長年議論されてきたヤコビアン予想を反証したこともある。

こうした動きは、数学界に期待と懸念の双方を広げている。6月には著名な数学者らが公開声明を出し、AIが数学の中核的な価値に影響を及ぼし得ると指摘した。

声明では、数学的証明は「発見の功績を帰し、その正確性に責任を負う特定の著者に帰属すべきだ」とする基準が揺らぎかねないとの懸念も示された。

一方で、AIが数学研究の手法そのものをより複合的に変えていくとの見方もある。フィールズ賞受賞者のティモシー・ガワーズは文章で、「数学の定理がもはや数学者と結び付かない世界が来たとしても、それは星が天文学者の名を冠していないという事実より大きな問題ではないかもしれない」と記した。

今回の成果は、AIがリーマン予想を完全に証明したわけではない。ただ、難問研究において、アイデアの生成と検証を役割分担型のエージェント構成で進められる可能性を示した点に意味がある。今後の焦点は、こうした手法が個別の定理証明を超え、数学界が受け入れられる一般的な発見の体系へとつながるかどうかにある。