グーグルのAIが56年未解決の数学問題を数百ドルで証明した

グーグル・ディープマインド（Google DeepMind）の研究システムが、数学者ポール・エルデシュ（Paul Erdős）が提起した九つの未解決問題について、機械で検証された完全な証明を生み出した。うち二つは56年間解かれていなかった。同じシステムは整数列オンライン百科事典から取った44の予想を片づけ、15年来開いていた代数幾何の問いを閉じ、凸最適化の既知の上界を改善した。目を引く数より方法が重要だ。これらの証明はどれも、機械が主張しただけでなく、機械が検証している。

1996年に亡くなったエルデシュは、正確で頑固な問いを数百も残した。多くは述べるのは簡単だが、決着させるのは恐ろしく難しい。数十年のうちに、それらはこの分野の常設試験のようになった。数列の予想は、数学者が規則性を探して掘り起こす公開データベースから来ており、推測された式が何年も証明されないまま残ることもある。これらはモデルを喜ばせるために作られた人工的な課題ではない。開かれた数学の本当の積み残しだ。

この区別がすべてだ。AlphaProof Nexusと呼ばれるこのシステムは、確認できない手順をどれも退ける形式言語Leanで論証を書く。証明は通るか通らないかのどちらかで、あとで誤りと分かる自信ありげな段落の入る余地はない。AIの「発見」が本物かどうかを見極めたい人にとって、ここがプレスリリースと結果との境界線になる。

おすすめ記事Opus 4.6に2ポイント差で5倍安い：Gemini 3.5 Flashが計算を書き換える

内部では、証明器はGemini 3.1 Proの上で動き、より軽いモデルが順位づけを担う。ループはほとんど退屈なほどだ。モデルがLeanで証明を書き、コンパイラがエラーを返し、そのエラーが次の試行に流れ込む。誠実さを保つのは流暢な文章ではなく、記号的なフィードバックだ。チームは複雑さの異なる四つの版を作り、うち一つは競合する証明の下書きを生成して順位づけする。それでも、最も単純な版、モデルとコンパイラだけのループが、九つのエルデシュ問題を独力で解いた。

ひそかに驚かされるのは費用の面だ。解けた問題一つあたりの計算時間は数百ドルだった。研究者の生涯を費やした問いが、週末旅行ほどの値段で閉じられた。これで数学者が引退するわけではない。どの問題に挑む価値があるかを選び、システムが読める形に書き換え、答えが何を意味するかを判断する人は依然として必要だ。変わるのは、そもそも何を試す価値があるかという計算である。

留保は見出しより重い。試した353のエルデシュ問題のうち九つの成功は、約2.5パーセントの的中率だ。数列の数字、492のうち44は、九パーセントを下回る。著者たちは率直に、これらの問題の大半は手の届かないところにあり、広範な新理論を要するものはなおさらで、成功はLeanの数学ライブラリがすでに充実した領域に集中していると認めている。人間が組んだその足場と、選び抜かれた標的のリストを取り去れば、システムに立つ場所はほとんど残らない。

この慎重さには理由がある。大いに嘲笑された出来事では、競合する研究所が自社モデルは十のエルデシュ問題を解いたと発表したが、数学者たちは答えがすでに公刊文献にあったと指摘した。モデルはそれらを見つけたのであって、証明したのではなかった。AlphaProof Nexusはその誤りに免疫を持つよう作られている。既知の結果のLean証明も有効な証明であり、本当に新しいもののLean証明は偽れない。ディープマインドを率いるデミス・ハサビス（Demis Hassabis）は、この成果は汎用人工知能ではないとわざわざ述べた。自社モデルにめったに控えめでない企業としては異例の慎重な注釈だ。

研究者たちが強調する、もっと目立たない収穫もある。失敗さえ役に立った。部分的な証明がどれも形式的に検証されるため、数学者は議論全体を手で確かめ直さずとも、システムがどの部分目標を閉じられ、どれを閉じられなかったかを正確に見られた。機械は神託であることをやめ、自らの作業を見せ、難所がまだどこに潜むかを指し示す、疲れを知らない協力者になる。

この結果は単独ではない。別の競合する推論モデルの主張とほぼ同じ時期に重なる。そのモデルは離散幾何のおよそ80年前のエルデシュ予想を反証したと報じられ、現役の数学者が精緻化し裏づけた。二つの研究所、二つの手法、一方は形式的検証に、もう一方は生の推論の連鎖に頼り、数週間の差で同じ最前線に達した。競争はもはや、賢そうに聞こえるチャットボットの話ではない。

この研究は今月公開された論文で説明され、手法はオープンな道具、すなわちLeanとコミュニティが築いたライブラリに依拠している。だから外部のグループは企業のブログを信じる代わりに、証明を検査し再実行できる。ディープマインドは、このシステムが社外の研究者の手に届くかどうかを明らかにしていない。注目すべき数字は九ではない。2.5パーセントが十になり、やがて二十になるかどうかだ。その日が来れば、これらの機械が何のためにあるのかという議論は、一から始め直さねばならない。

関連記事

SpaceXの上場目論見書、AnthropicがColossusに年150億ドル支払いと明示

DeepSeekがAIを安くした、米国のAIバブルは「高止まり」に賭けていた

OpenAIの汎用モデル、数学専用ではないのに80年来の幾何予想を解く

マイクロソフト、Anthropicを社外初のMaia 200顧客にする交渉へ