Google DeepMindのAlphaProofは、数学の証明を形式言語Leanで生成し、機械的に検証できる形で解くAIである。国際数学オリンピック（IMO）2024では、AlphaGeometry 2と合わせて銀メダル水準の成績とDeepMindが発表した。その後、IMO 2025では上位モデルによる金メダル水準の成果が報告されるなど、進展が続いている。評価の枠組みを正確に押さえることが理解の前提である。

AlphaProofとは：Leanで検証される形式証明の生成

AlphaProofは強化学習で証明探索を行うシステムで、約100万規模の問題を形式化した学習データを使うと説明されている。自然言語の答案と違い、Leanで書かれた証明は一歩ずつ正しさを機械検証できるため、『答えが合っているか』ではなく『論証が成立しているか』を担保できる点が本質である。幾何専門のAlphaGeometry 2と役割を分け、代数や数論などはAlphaProofが担う構成でIMOに挑んだ。

IMOでの評価：銀メダル水準から金メダル水準の報告へ

IMO 2024での評価は、大会の問題を形式化し、制限条件のもとで解いた結果を専門家が採点して銀メダル相当とされたもので、公式参加者としてのメダルではない。2025年にはDeepMindの高度なモデルが金メダル水準の解答を出したと発表され、他社からも同様の報告が出るなど競争が進んだ。これらは各社の発表に基づく情報であり、条件の違いを揃えた横比較は難しい点に注意が要る。

形式証明AIの意味：検証可能性が科学応用へつながる理由

実務的な意味は、競技数学そのものより、検証可能な推論の自動化にある。ソフトウェアの形式検証や、科学計算の正しさを要する領域では、生成と検証を分ける設計が信頼の基盤になる。日本のAI研究者にとっては、評価問題の形式化コストが依然として大きく、人手による問題整備がボトルネックである点も論文・発表から読み取れる論点である。

AI研究者は、生成モデルの出力を検証器で担保する設計思想を自領域へ応用できる。教育関係者は、競技の成績を『AIが数学者を超えた』と短絡しない読み方を生徒にも伝えたい。成績は各年次の発表条件に基づく。

あわせて読みたい

「研究成果が事業にならないのはなぜか：技術・顧客・資金の3つの断絶」 https://seed.aohalab.ai/#/article/2

「TRL（技術成熟度）の読み方：研究の現在地を測る物差し」 https://seed.aohalab.ai/#/article/21

出典：Google DeepMind発表「AI achieves silver-medal standard solving problems from the International Mathematical Olympiad」（2024年7月） https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

本記事で紹介した内容は2026年11月時点の公表情報に基づきます。最新の内容は出典の一次情報をご確認ください。