発表
2026年10月8日、科学誌 Science は Google DeepMind の AlphaProof Nexus に関する査読済み論文("Advancing mathematics research with AI-driven formal proof search")を掲載しました。プレプリントは5月21日から arXiv にありました。このシステムは、LLM ベースのエージェント が Lean で書かれた証明を探すものです。Lean ではコンピューターが証明のすべてのステップを 機械的に検証 します。
成果
論文によると:
- 挑戦した エルデシュ問題353問のうち9問 を自律的に解決(約2.5%)。うち 2問は56年間未解決 でした(1970年にエルデシュとサールケジが提起した #12(i)、#12(ii))。推論コストは 1問あたり数百ドル
- オンライン整数列大辞典(OEIS)の 予想492件のうち44件 を証明
- 代数幾何の ヒルベルト関数に関する15年来の問題 を解決し、凸最適化 の上界を改善、Ben Green のリストの問題解決にも貢献
- 文献中の 形式化の誤り を発見
Lean の証明は GitHub の google-deepmind/alphaproof-nexus-results(Apache 2.0、約300スター)で公開され、Terence Tao 氏の AI 貢献 wiki にも記録されています。
仕組み
- エージェント A: シンプルなループ。LLM(Gemini 3.1 Pro)が案を出し、Lean コンパイラーが検証し、エラーをモデルに返して繰り返す
- エージェント D(完全版): 投票と Elo 評価を使う 進化的アルゴリズム でサブエージェントを協調させ、強化学習で鍛えた証明器 AlphaProof も呼び出せる
最も興味深い注意点
事後分析では、シンプルなループのエージェント A が、完全版と同じ9問のエルデシュ問題を解いていました(最難問ではコストが高め)。スペインの Science Media Centre の取材に応じた Josep Curto 氏(UOC)は、決め手は複雑な構成ではなく 強い LLM と厳格な検証器からのフィードバック だと指摘し、コストが成功した実行だけを数え、AlphaProof の推論を除いている点も批判しています。
ほかの注意点:
- Lean でも幻覚はなくならない: 保証されるのは Lean で書かれた命題 に対する正しさで、その命題が元の問題を正しく表しているかは別です。チームは専門家が各命題を確認しました
- 無作為の標本ではない: 353問は1,200問以上のうち、すでに Lean で形式化された問題です
- Javier Aramayona 氏(ICMAT)らは、正しいと証明されても誰も本当には理解していない結果 が増えることに警鐘を鳴らしています
数学以外での意味
「生成して検証する」 パターンはあらゆる AI エージェントに使えます。モデルが提案し、客観的な検証器(コンパイラー、自動テスト、スキーマ検証、業務ルール)が採否を決めます。企業にとっては:
- 自動検証なしにエージェントの出力を信用しない。 テスト、リンター、バリデーターをループに入れる
- シンプルに始める: 良いモデルと厳格なフィードバックが複雑な構成に勝つことが多い
- 仕様を確認する: 検証器は頼んだことしか保証しません
- 失敗した試行も含めて 総コストを測る
出典
- Science, doi 10.1126/science.aej2213 (8/10/2026)
- arXiv 2605.22763: https://arxiv.org/abs/2605.22763
- GitHub, google-deepmind/alphaproof-nexus-results: https://github.com/google-deepmind/alphaproof-nexus-results
- Science Media Centre Spain: https://www.sciencemediacentre.es/en/alphaproof-nexus-new-ai-tool-designed-tackle-mathematical-proofs
- postcutoff: https://postcutoff.com/e/2026-10-08-alphaproof-nexus-science-paper/
検証を組み込んだ AI エージェントを業務に導入したいですか?KGA IT は無料相談を受け付けています:kga-it.com