【全４回連載（第１回）】AIが数学の証明を書けるようになった6年間 ── Neural Theorem Proving の全体像を、正答率30%から99.6%への軌跡とともに読む

はじめに

本記事は、全４回の連載記事の１本目です。

すでに 公開済みの別の連載記事シリーズ『コードなのに、そのまま数学の証明文として読める』（前編・後編） では、第１回でタクティクスタイル の読みにくさを、第２回で宣言的スタイル の30年を扱いました。

• 【過去に公開済みの記事】コードなのに、そのまま数学の証明文として読める ── AIが証明を書く時代に注目すべきMizar・Isabelle・Lean 4 の宣言的スタイルの記法
   
• 【過去に公開済みの記事】コードなのに、そのまま数学の証明文として読める ── AIが証明を書く時代に注目すべきMizar・Isabelle・Lean 4 の宣言的スタイルの記法

いま皆様がアクセスしてくださっている この記事 から始まる 全４回の新連載シリーズ は、AIに定理証明を学ばせる Neural Theorem Proving 研究 の 『2020年から2026年まで』を、時系列で追いかけます。

本連載は全４回の構成

この主題は、一本の記事に収まりません。

そこで、４回に分けてお届けします。

各回で扱うこと

第１回（この記事）── 用語と歴史

Neural Theorem Proving という研究分野に登場する 専門用語 について、まず最初に解説します。

その上で、この研究領域の 1997年から2025年まで を時系列でたどります。

GPT-f、miniF2F、Draft Sketch and Prove、LeanDojo、AlphaProof、Seed-Prover。

以上の流れを追いかけた上で、miniF2F という問題集を、AIがほぼ学習し尽くした感のある様子 を取り上げます。

第２回 ── AIの内部構造

数学の定理などに関する証明 を 自動的に生成する Neural Theorem Prover は、Lean 4 や Rocq、Isabelle などの定理証明支援系がもちいる ２つのスタイルの記法 である タクティク記法 と 宣言的スタイルの記法 のうち、どちらのスタイルで学び（モデル学習を行い）、どちらのスタイルの証明を書く（生成する）のか？

複数の代表的な Neural Theorem Prover に入力される学習データ と、Neural Theorem Prover から生成される証明の例 を、皆様と一緒に見ていきたいと思います。

第３回 ── 誰が動かしているか

この分野を牽引する研究者と組織、国家 について見つめます。

第４回 ── 何が争われているか

「証明は正しいが、定理が間違っている」という問題 に光を当てます。

さらに、「そもそも形式化は必要か」という立場の隔たり、AIの貢献をどう記録するか、費用の実態と、ビジネスへの応用 といった論点を取り上げます。

全４回の記事： 全体構成

各記事 は、主題が切り替わる箇所 で分けました。

主題の切り替わり は、以下のとおりです。

第１回と第２回の境界 ── 第１回は「何が起きたか」の記録です。時系列に沿った物語です。第２回は「どう作られているか」の解説です。技術的な内部構造を探ります。

第２回と第３回の境界 ── 第２回までは「仕組み」の話です。第３回は「人と組織」の話になります。

第３回と第４回の境界 ── 第３回までは「事実関係」を扱います。第４回は「何が問題か」を論じます。

各回は、単独でも読めるように書いています。

各回でカバーされる章節番号("部"の番号)の範囲は下記のとおりです。

第１回： 第１部 ～ 第８部、
第２回： 第９部 ～ 第10部、
第３回： 第11部 ～ 第12部、
第４回： 第13部 ～ 第17部

この初回記事の要約

2020年、AIは「証明の一手」を生成し始めました。

2025年、AIは高校数学の形式証明の問題集を、ほぼ学習し尽くしました。

2026年、AIは人間が立てた未解決問題を、実際に解き始めました。

しかし、「新しい問いを立てる」段階には、まだ大きな隔たりがあります。

この初回記事が立てる 問い

AIは「人間が立てた定理を証明する仕組み」から、「自分で数学の問いを立て、証明し、さらに次の問いを生み出す仕組み」へ進めるのでしょうか。

この問いを、研究論文とともに追います。

本記事について３つの断り書き

（１点目）なぜ「６年間」なのか。

本記事では、2020年の GPT-f を、現在のニューラル定理証明の大きな転換点として扱います。

この記事が取り上げる ６年間 とは、この 2020年という年から、この記事を執筆している2026年までの６年間 です。

（２点目）タイトルにある「30%から99.6%」について。

この数字は、同一の条件で測定された単純な時系列ではありません。

代表的な研究成果を通じて、この分野の進歩を俯瞰した数字です。

個々の数値は、モデルの規模も試行回数も、使った問題集の版も異なります。

（３点目）本記事で「確認できませんでした」と書く箇所について。

この記述は、「存在しない」という事を断定するものではありません。

本連載の執筆時点で、筆者が調べた範囲では見つけられなかった、という意味です。

対話篇でお伝えする『本記事の主題』

この分野が何を目指しているのかを、対話の形で整理します。

登場するのは、タロウくん（機械学習に携わるエンジニア。過去に公開済みの記事（タクティクスタイル）と過去に公開済みの記事（宣言的スタイル）を読んでいる）と、専任講師です。

タロウくん：
先生、これまでの２回で、定理証明支援系というものを知りました。

専任講師：
はい。

タロウくん：
有名な数学の難問の証明 が 正しいかどうか 。

OSの実装コード が 仕様から外れた振る舞いをしないかどうか 。

それを確かめるために、論理の飛躍を見落とさない処理系へ入力できる形式言語に翻訳 する。

その作業だけで、１０年規模の時間がかかるという話 でした。

専任講師：
そのとおりです。

タロウくん：
この所要時間を、一気に短縮するのが目的 ですか？

専任講師：
それが、この分野の出発点です。

タロウくん：
つまり、これまで人間が書いてきた形式化されたコードを、学習データとして、AIに学ばせる。

そして、「この数学の定理を証明する形式化コードを出力しなさい」とAIに依頼する。

そういうことでしょうか。

専任講師：
正確です。

そして、その依頼の仕方には２通り あります。

タクティクを一手ずつ出力 させるか、
証明を丸ごと出力 させるか。

タロウくん：
過去に公開済みの記事で見た、２つのスタイルですね。

専任講師：
そうです。

タロウくん：
もう一つ、伺いたいことがあります。

専任講師：
どうぞ。

タロウくん：
いま先生がおっしゃったのは、「すでに人間が立てた予想 を、AIが証明する」という話です。

専任講師：
はい。

タロウくん：
しかし、AIが、まだ人間が発見していない数学の定理を見つける ことも、目指されているのでしょうか。

専任講師：
目指されています。

その話をする前に、まずすでに達成されたことをご紹介させてください。

タロウくん：
お願いします。

すでに人間が提唱していた予想を、AIが人間より先に証明した

専任講師：
2026年5月のことです。

Google DeepMind が AlphaProof Nexus という仕組みを発表しました。

タロウくん：
何をしたのですか？

専任講師：
未解決だったエルデシュの問題353問 に挑み、９問を自律的に解決 しました。

そのうち ２問 は、56年間、誰も解けずにいたもの です。

タロウくん：
エルデシュの問題 というのは。

専任講師：
ポール・エルデシュという20世紀の数学者が残した、未解決の問題群 です。

インターネット上に1,200問を超える目録があり、その一部が Leanで形式化 されています。

タロウくん：
それをAIが解いた。

専任講師：
さらに、OEISの未解決の予想492問 のうち、44問も証明 しています。

タロウくん：
OEIS というのは？

専任講師：
整数列大辞典（ Online Encyclopedia of Integer Sequences ）です。
数列に関する予想 が、大量に集められています。

タロウくん：
その結果は、数学者に認められたのですか。

専任講師：
論文によれば、解決のたびに、研究チームの専門家が 「Lean で書かれた主張が、元の予想を忠実に捉えているか」を検証 しています。

出典
George Tsoukalas, Anton Kovsharov, Sergey Shirobokov ほか（Google DeepMind）, "Advancing Mathematics Research with AI-Driven Formal Proof Search", arXiv:2605.22763, 2026年5月21日

そしてその成果は、テレンス・タオが管理する「エルデシュ問題へのAIの貢献」という記録に登録 されました。

タロウくん：
先生、費用はどのくらいかかるのですか？

専任講師：
論文には「１問あたり数百ドル」と書かれています。

タロウくん：
・・・安いですね。

専任講師：
この仕組みの入力が、興味深いのです。

タロウくん：
入力、ですか。

専任講師：
論文にはこうあります。

「エージェントは、証明の代わりに sorry を置いた目標の定理と、それが依存する定義とライブラリの読み込みからなる Lean ファイルを、入力として受け取る」と。

タロウくん：
sorry は、過去に公開済みの記事で出てきた語です。
「この部分は、まだ証明していません」という印 でした。

専任講師：
そのとおりです。

人間が骨組みを書き、穴を空けて渡す。AIがその穴を埋める。

タロウくん：
過去に公開済みの記事で学んだ書き方が、そのまま使われているのですね。

専任講師：
この連載が扱ってきたものが、いま最前線で使われています。

では、AIは新しい予想を立てられるのか

タロウくん：
先生、いま伺ったのは、人間がすでに提唱していた予想 を、AIが証明したという話ですよね？

専任講師：
そのとおりです。

エルデシュの問題も、OEIS の予想も、人間が立てたもの です。

タロウくん：
私が伺いたかったのは、その先です。

AIが、まだ人間が誰も思いついていない新しい予想を、自分で提示することは、目指されているのでしょうか。

専任講師：
目指されています。

そして、その研究には 長い歴史 があります。

タロウくん：
長い歴史、ですか。

LLMが登場して以後の話だと思っていました。

専任講師：
1980年代からあります。

タロウくん：
・・・そんなに前から。

専任講師：
Siemion Fajtlowicz という数学者が、GRAFFITI という仕組みを作りました。

グラフ理論の不等式について、計算機が自動で予想を立てる のです。

タロウくん：
名前が変わっていますね。

専任講師：
「壁に書かれた落書き」という意味です。

他の数学者が見られるように、予想を壁に貼り出すという含みがあります。

タロウくん：
その予想は、役に立ったのですか。

専任講師：
エルデシュ、ファン・チャン、ファーバーといった数学者たちの注目を集めました。

そして後継の仕組みも作られています。

• GRAFFITI.pc
• Conjecturing
• AGX
• Graphedron

そして 2017年 の TxGraffiti です。

タロウくん：
では、AIが新しい予想を立てるのは、もう実現しているのですね？

専任講師：
そこが微妙なところです。

タロウくん：
微妙、ですか？

専任講師：
これらの仕組みが立てるのは、主にグラフの不等式です。

数値の表を計算し、成り立ちそうな関係を探す。

数学の広い領域にわたって、新しい概念や新しい問いを提示するものではありません。

タロウくん：
なるほど。

専任講師：
そして2026年、LLM を使った予想生成の研究が現れました。

タロウくん：
どういう仕組みですか？

専任講師：
まず、LLMに予想を書かせます。

そして Lean の exact? という命令で、その予想が既存のライブラリから即座に導けないかを確かめる。

導けてしまうなら、それは新しくないということ です。

タロウくん：
新しさを、機械的に判定するわけですね？

専任講師：
そのとおりです。

「Mathlib にまだ無いこと」を、新しさの目安にしています。

タロウくん：
それで、成果は出ているのですか？

専任講師：
ここは、正確に事実をおさえないといけない部分です。

筆者が調べた範囲では、「AIが自分で立てた新しい予想が、数学の共同体に重要なものとして受け入れられた」という事例は、確認できません でした。

タロウくん：
・・・まだ、ないのですか。

専任講師：
2026年8月11日の時点では、そう言わざるを得ません。

アルベルト・ロメロという評論家が、この分野の現状を次のように評しています。

（原文引用）

The Riemann hypothesis lies on the horizon, like a final boss. And yet—no new math, no new conjectures, no new interesting ideas, no novel premises.

（筆者による日本語訳）

リーマン予想が、最後の関門のように地平線上に横たわっている。
それでもなお、新しい数学も、新しい予想も、新しい興味深いアイデアも、新しい前提もない。

出典
Alberto Romero, The Month AI Conquered Math: The Full Story, The Algorithmic Bridge, 2026年8月

この人物は、The Algorithmic Bridge という媒体を主宰しています。

AIを人間の側から論じる、購読者数万人規模のニュースレターです。

タロウくん：
厳しい評価ですね。

専任講師：
ただし、注意してほしいことがあります。

この評価は、AIの成果を否定するものではありません。

タロウくん：
と言いますと。

専任講師：
同じ評論家は、こうも書いています。

「４年で、AIは自分の意思を伝えることもできない状態から、あなたが理解できないような100年来の数学を解くところまで来た」と。

タロウくん：
・・・両方とも事実だ、ということですか？

専任講師：
そうです。

人間が過去に発見済みの数学の予想を証明する力は、驚くほど伸びました。

しかし、新しい、未発見の数学の予想を立てる力については、まだ何とも言えません。

タロウくん：
先生、リーマン予想を解くことと、リーマン予想を思いつくことは、違うということですね。

専任講師：
まさに、そう指摘されています。

「リーマン予想を解いたからといって、その人がリーマンになるわけではない。リーマンは、そもそもそれを思いついたのだから」と。

タロウくん：
・・・なるほど。

専任講師：
ただし、最後に一つ、興味深い事実をお伝えします。

タロウくん：
何でしょうか。

専任講師：
先ほどお話しした AlphaProof Nexus が、グラフ理論のある予想を証明しました 。

そして、その予想を立てたのは、1996年のGRAFFITI だった んです。

タロウくん：
先生がさっき、1980年代の仕組みとして紹介されたものですか？

専任講師：
そうです。

機械が立てた予想を、30年後に別の機械が証明したわけ です。

タロウくん：
輪がつながった、ということですね？

専任講師：
論文自身が、そう書いています。

「これは、AIによる予想とその証明のあいだで輪を閉じるという、興味深い将来の可能性を指し示している」 と。

タロウくん：
「将来の可能性」。

専任講師：
そうなんだ。

まだ 輪は閉じていない。だから、まだ将来の可能性なんだ。

予想を立てる仕組みと、証明する仕組みは、別々に存在している。
それが一つの流れになるかどうかは、これからの話です。

この論点については、判断が分かれています。

筆者としては、次のように整理しておきます。

「予想を立てる」研究は、1980年代から続いており、LLM を使ったものも2026年に現れました。

しかし、その成果が数学の共同体に受け入れられた事例は、本連載の執筆時点では確認できていません。

出典

• Siemion Fajtlowicz の GRAFFITI と、その後継について:"Computer assisted discovery: Zero forcing vs vertex cover", arXiv:2209.04552
   
• TxGraffiti の10年間:"In Reverie Together: Ten Years of Mathematical Discovery with a Machine Collaborator", arXiv:2507.17780
   
• LLM による予想生成:"Discovering New Theorems via LLMs with In-Context Proof Learning in Lean", arXiv:2509.14274
   
• 現状への評価:The Month AI Conquered Math: The Full Story, The Algorithmic Bridge, 2026年8月
   
• AlphaProof Nexus:George Tsoukalas, Anton Kovsharov, Sergey Shirobokov ほか（Google DeepMind）, "Advancing Mathematics Research with AI-Driven Formal Proof Search", arXiv:2605.22763, 2026年5月21日
   
• OpenAI の非公開モデルによるエルデシュ予想の解決:Boris Alexeev, Moe Putterman, Mehtaab Sawhney, Mark Sellke, Gregory Valiant, "Short proofs in combinatorics and number theory", arXiv:2603.29961, 2026年、および "Short proofs in combinatorics, probability and number theory II", arXiv:2604.06609, 2026年

なお、テレンス・タオは、2026年7月の国際数学者会議 で、「Mathematics in the age of AI」という講演 を行っています。

この分野が、数学という学問そのものにどう影響するのかは、本記事の範囲を超えます。
関心のある方は、講演の資料をご覧ください。

出典
Terence Tao on AI in mathematics (and beyond)

最初に、この分野の全体像 を示します。

AIは何を学習データにしているのか

人間が書いた形式証明のコードそのもの です。

具体的には、

• Lean の Mathlib（数学ライブラリ）
• Isabelle の AFP（Archive of Formal Proofs）
• Coq や Metamath の証明集

です。

これらは、人間の研究者が何十年もかけて書き溜めたもの です。

これらは有限です。

そして、人間が書く速度には限りがあります。

では、どう対処しているのでしょうか。

大きく分けて、３つの方向があります。

【対処策１】 解けた証明を学習データに戻す

第１部で扱う専門家反復です。

AIに問題を解かせ、解けたものだけを選び、それを学習データに加える。

この繰り返しです。

しかし、この方法には限界があります。

あるサーベイ論文は、こう指摘しています。 未証明の定理に対して正しい証明を生成するために必要な標本の数が、指数的に増大してしまう。そのため性能はすぐに頭打ちになる、と。

【対処策２】 モデルに問題を作らせる

第６部で扱う STP がこれにあたります。

モデルが予想を立て、それを証明し、成功した証明を学習データに戻す。

【対処策３】 大きなモデルが小さなモデルの教材を作る

本連載の第２回の記事の第９部で扱う DeepSeek-Prover-V2 の手法です。

大きなモデルが証明の素描を作り、小さなモデルが埋め、その組み合わせを学習データにします。

これ以外の対処策

もう一つの方向性があります。

武漢数学与智能研究院 の楊志堅の提言をとりあげます。

【コラム】武漢数学与智能研究院 と 楊志 堅氏について

武漢数学与智能研究院（英語名 Institute for Math & AI, Wuhan）は、武漢大学の実体研究機関です。

2023年6月に設立されました。比較的新しい組織です。

公式サイト
https://imai.whu.edu.cn/

楊 志堅氏について

現在の肩書きは、次のとおりです。

• 武漢大学 弘毅特聘教授
• 湖北国家応用数学中心 主任
• 武漢数学与智能研究院 副院長

経歴も記しておきます。

北京大学で学士と修士を修めた後、プリンストン大学で博士号を取得。カリフォルニア工科大学で博士研究員を務め、ロチェスター工科大学で助教を経て、2010年に武漢大学へ移りました。

専門は、多尺度モデリングと計算、そして人工知能の数学的理論です。

本記事では「湖北省数学学会の理事長」と記しました。

ただし、資料によっては「湖北省工業与応用数学学会の理事長」という記述も見られます。

両方の役職を兼ねているのか、あるいは資料の時点が異なるのか、筆者には判別できませんでした。

出典

• 武汉数学与智能研究院
• 杨志坚教授课题组 博士后招聘启事

本連載の第３回の記事の第１１部で扱う予定です。

AI には「３本の足」がある。データ、計算力、アルゴリズムである。そのうち数学界が最も力を発揮できるのはデータの領域であり、数学専用のデータ集合の構築や、データ標準の確立といった基礎的な仕事である。

つまり、数学者が形式化を進めることで、学習データを増やすという考えです。

ここで、「形式化」という専門用語 について、説明させていただきます。**

数学の教科書や論文に書かれた証明は、日本語や英語の文章 です。

• 「明らかに」
• 「同様にして」

などと書いて、途中の証明過程の記載を省略することもあります。

形式化 とは、そのような証明文を、 定理支援証明処理系 である Lean や Isabelle が読める形へと 書き直す作業工程を指す言葉 です。

• 「明らかに」
• 「同様にして」

などと、記述を省略した箇所も、すべて厳密にコードに書き表さなくてはなりません。

定理証明支援処理系は、「明らかに」を受け付けないから です。

定理証明支援系のコードに置き換えられた証明（コード）は、定理証明AI（ Neural Theorem Prover ）が学習データとして受け取れる 状態になります。

実際に、定理証明AIが、定理支援証明のコードを学習する動き（研究）は、複数の国々ですでに始まっています。

そして、その学習データを支えているのが、数学者たちの長年の蓄積です。

Lean には Mathlib、Isabelle には Archive of Formal Proofs と名付けられた 形式化された証明 を集めた ライブラリ があります。

Mathlib は、世界中の数学者の貢献が積み重なって、今日まで成長してきました。
Archive of Formal Proofs も同じです。

この２つについて、少し補足します。

Mathlib は、Lean 4 のための数学ライブラリです。
数十万の定理が登録されており、代数、位相、解析、数論など、数学の広い範囲 をカバーしています。

全体が一つの体系としてつながっており、新しい数学の定理は、既存の枠組みの中へと組み込まれていきます。

数学の教科書を、一冊ずつ積み上げていくような形です。

Archive of Formal Proofs（AFP）は、Isabelle のためのアーカイブです。

査読があり、学術誌のように運営されています。

こちらは一枚岩ではなく、独立した記事の集まりです。

著者も目的も異なるものが、並んで収蔵されています。
そして、数学の定理だけではなく、そのおよそ半分は、ソフトウェアの検証を扱っています。

どちらも、人間が何十年もかけて書き溜めたものです。

そして、その蓄積が、いま AIの学習データになろうとしています。

【筆者の見解】

ここに、興味深い循環があると筆者は考えます。

AIが形式化を助ければ、形式化された数学が増えます。

形式化された数学が増えれば、AIの学習データが増えます。

この循環 が回り始めれば、データの枯渇 という、定理証明AIの学習データの量にまつわる制約を緩和することができると思われます。

しかし、この循環の中に、「形式化の誤り」（misformalization） が混入すれば、誤りも増幅 されます。

ここで言う「形式化の誤り」（misformalization）とは、次のようなことです。

数学の問題 を Lean へ 翻訳 したとき、書き写した主張が、元の問題と食い違ってしまう。
これを、「形式化の誤り」 と呼びます。

そして厄介なことに、その主張の証明は、Leanの処理系で正しく動く、正しいLeanのコードとして書かれてしまいます。

Lean がしてくれることは、「書かれた主張が証明されているか」を確かめるだけで、「その主張が、元の問題の題意を忠実に、適切に反映しているか」までは確かめてくれないのです。

つまり、検査を通った証明が、見当違いのことを証明しているという事態が起こりえます。

この誤った証明が学習データに戻れば、次の世代のAIは、それを手本として学んでしまうこととなります。

その問題は、本連載の第４回の記事で扱います。

なお、この論点については、筆者が以前に公開した記事でも扱っています。

• 形式証明は「仕様が人間の意図を反映しているか」は保証しない ── Correctness と Appropriateness の境界

処理系が保証するのは「正しさ」であって、「適切さ」ではない。 その境界を論じた記事です。

そして、実務のコード検証の側から同じ問題を扱った記事もあります。

• 「テスト通ったから大丈夫」を卒業しよう ── LLM生成コードをLean4/Dafnyで形式検証する方法

そこでは、形式検証で「まだ難しいこと」の一つとして、仕様そのものの正しさを挙げています。仕様が間違っていれば、検証も無意味である、と。

数学の定理証明でも、実務のコード検証でも、同じ落とし穴があります。

どんなタスクを解いているのか

分類でも回帰でもありません。生成タスク です。

そして、生成の仕方には、２つの流儀 があります。

• 一手ずつ生成する（step-level generation）── 「いまの証明状態」を入力し、「次のタクティク１つ」を出力する。出力を処理系に渡し、返ってきた新しい状態をまた入力する。この繰り返しです
   
• 証明を丸ごと生成する（whole-proof generation）── 定理の主張だけを入力し、証明全体を一度に出力する。そして処理系に検査させる

一手ずつ生成する場合。

証明を丸ごと生成する場合。

最終的な証明の成否は、形式検証を通るかどうかという二値で判定できます。 処理系の検査を通れば正解、通らなければ不正解。部分点はありません。

ただし、研究の評価そのものは二値ではありません。何回試したか、どれだけの計算資源を使ったか、生成された証明がどれだけ長いか。そうした指標も併せて報告されます。この点は、後で詳しく扱います。

どのくらいの精度なのか

最もよく使われる 問題集 は、 miniF2F です。

高校の数学オリンピックなどから採った488問を、形式言語で書き直したものです。

その正答率は、以下のように推移していきました。

年	正答率	システム
2021年2月	29.6%	Proof Artifact Co-training
2024年10月	33.6%	TheoremLlama（8Bのモデル）
2025年9月	99.2%	Hilbert
2025年	99.6%	Seed-Prover

なお、この表は「最高記録の時系列推移」ではありません。

代表的なシステムを並べたものであり、同じ年にこれより高い成績を出したシステムも存在します。

また、試行回数などの条件も研究ごとに違います。

その点は、第６部で詳しく扱います。

244問中243問。残る未解決は１問だけです。

この問題集を、AIはほぼ学習し尽くしてしまいました。

そろそろこの問題集を卒業し、より難しい大学の学部から大学院の水準の問題へ移るべき時なのかもしれません。

ただし、これは高校レベルの問題です。

数学者が実際に取り組んでいる問題との隔たりは、まだ大きく残っています。

AIは、どちらのスタイルを学び、どちらのスタイルで書いているのか

学習データも、生成されるコードも、両方のスタイルが混ざっています。

そして、その混ざり方には、はっきりした型があります。

AIは、have で中間の主張を宣言し、その中身をタクティクや自動化で埋めています。

Lean 向けのモデルも、Isabelle 向けのモデルも、同じ形です。

過去に公開済みの記事の最後で「タクティクで探し、宣言的スタイルで残す」と書きました。

Neural Theorem Prover の研究 では、その順序が逆 になっています。

「宣言的スタイルで骨格を立て、タクティクで埋める」

ただし、have が並んでいれば読みやすいわけではありません。

その have が、本当に論証の筋道を示しているかどうかについては、議論があります。

この論点は、本連載の第２回の記事の第９部で、実際に生成されたコードを見ながら詳しく扱います。

過去に公開済みの記事で、sorry という語を説明しました。「この部分は、まだ証明していません」と処理系に伝える印です。

この仕組みが、いま研究の中心にあります。

2025年の ProofAug という研究では、次のように定義されています。

By semi-proofs, we refer to proofs that possibly contain symbols indicating pending proof, such as sorry in Isabelle and Lean.

筆者による日本語訳

semi-proof（部分的な証明）とは、証明が保留であることを示す記号、たとえば Isabelle や Lean における sorry を含みうる証明のことを指す。

出典
Haoxiong Liu, Jiacheng Sun, Zhenguo Li, Andrew C. Yao, "ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis", ICML 2025, 39568〜39586頁

1997年に人間が証明を書くために提案された手法が、2020年代にAIの手法として使われているということです。

その経緯を、これから時系列で追います。

この記事について

過去に公開済みの記事（タクティクスタイル）と過去に公開済みの記事（宣言的スタイル）を読まれた方を、想定読者としています。

• 【過去に公開済みの記事】タクティクスタイルの読みにくさを扱った回
• 【過去に公開済みの記事】宣言的スタイルの30年を扱った回

ただし、この記事で初めて登場する用語や概念は、すべて第１部で説明します。

想定読者

• 過去に公開済みの記事（タクティクスタイル）と過去に公開済みの記事（宣言的スタイル）を読まれた方
• Python は書けるが、形式手法や定理証明支援系は専門ではない方
• 機械学習に携わっており、この分野の全体像を知りたい方
• AIが数学やソフトウェア検証にどう関わるのかを、数字で把握したい方

この記事を読む価値

1. AIに定理証明を学ばせる研究の、2020年から2026年までの全体像が分かる
    
2. Neural Theorem Proving という分野名と、その主要な用語を知る
    
3. miniF2F の正答率が、約30%から99.6%へ推移した経緯を、論文とともに追える
    
4. なぜ Lean のほうが研究が多く、成績も高いのか。その理由が分かる
    
5. 宣言的スタイルが、AIの研究でどう扱われているのか。４つの異なる方向を知る
    
6. この分野を牽引しているトップランナーたちの所属と系譜が分かる
    
7. 日本、アメリカ、中国、フランスの動向を、国家政策と実際の研究の両面から知る
    
8. 「そもそも形式化は必要か」という、この分野の中心にある対立を知る
    
9. 「証明は正しいが、定理が間違っている」という問題を知る。形式化の誤りは、AIによって深刻になる
    
10. いくらかかるのか。試行回数と費用の実態が分かる
     
11. 自分でこの分野を追いかけるための手がかりが得られる

TL;DR

（この節の専門用語は、いずれも本文で説明します）

Neural Theorem Proverモデルについて

• AI定理証明の土台になっているのは、人間が蓄積してきた形式証明である。 Lean の Mathlib、Isabelle の AFP など
   
• しかし現在は、AI自身が生成した証明を学習データへ戻す循環も始まっている
   
• タスクは生成である。 一手ずつ生成する方式と、証明を丸ごと生成する方式がある。最終的な成否は形式検証を通るかどうかの二値だが、試行回数や計算資源も併せて評価される
   
• miniF2F という問題集 の正答率は、2021年の約30%から、2025年の99.6%へ推移した。AIはこの問題集をほぼ学習し尽くした印象がある
   
• ただし、これは高校レベルの問題に取り組んだ結果である。 研究者レベルの数学との隔たりは、いまだに大きい
   
• 学習データは有限である。 人間が書いた形式証明の量には限りがあり、専門家反復、自己対戦、大きなモデルによる教材の生成といった手法で補われている

どちらのスタイルで書いているのか

• 少なくとも本連載で取り上げた研究では、AIが生成する証明に、宣言的な骨格とタクティクを組み合わせた構造が見られる。 have で中間の主張を宣言し、その中身をタクティクや自動化で埋める形である
   
• 主要なAIの入力は、一貫して「形式言語で書かれた主張」である。 日常の言葉から形式言語への翻訳は、AlphaProof の時点では人間が行っていた
   
• そして学習データの作り方が、時代とともに変わった。 2020年は人間が書いた証明をそのまま使ったが、2025年にはAIが自分で教材を作るようになっている
   
• 学習データ自体が二層構造である。 大きなモデルが証明の素描を作り、小さなモデルがその部分目標を埋める。その両方を組み合わせたものが学習データになる
   
• ただし、have が並んでいれば読みやすいわけではない。 ある論文は「最初の数行は自明な変形で、最後の一行が一気に片付けている」と自ら述べ、別の論文は生成された証明を「冗長」と評している
   
• Lean の記録が99.6%、Isabelle の記録が66.0%。 しかし差を生んでいるのは言語の優劣ではなく、ライブラリの規模と、問題集の性質である

何が達成され、何が未達成なのか

• 2026年、AIが未解決のエルデシュ問題を証明した。 AlphaProof Nexus は353問中９問を自律的に解決している。うち２問は、56年間、誰も解けずにいた問題である
   
• その入力は、sorry を置いた Lean ファイルである。 過去に公開済みの記事で説明した仕組みが、最前線で使われている
   
• しかし、AIが自分で新しい予想を立て、それが数学の共同体に受け入れられた事例は、確認できていない
   
• 宣言的スタイルについては、４つの方向の研究がある。 言語を作り変える、書き方を定める、変換する、移植する
   
• 形式的な証明が正しくても、その主張が元の問題と違っていることがある。 これを形式化の誤り（misformalization）と呼ぶ。ProofNet の Lean 4 版には、全体の31.8%にあたる118件の誤りが含まれていた

この分野の研究の牽引者（トップランナー）たち

• Neural Theorem Proving と名付けられたこの研究領域 は、ケンブリッジ大学、エディンバラ大学、カーネギーメロン大学、Mistral AI、xAI、Google DeepMind、DeepSeek、ByteDance などによって牽引されている
   
• 日本にも、世界水準の研究がある。 京都大学・東京大学・国立情報学研究所の Prover Agent は、8Bの小型モデルで miniF2F 88.1%。小型モデルの手法として世界最高であり、試行回数は従来の４分の１
   
• 中国では、定理証明を名指しした国家プロジェクトは確認できなかった。 しかし国務院の「人工知能+」行動の意見が「AI+科学技術」を筆頭に掲げ、その下で企業と大学が個別に激しく競争している
   
• フランスは、この分野の土台を作った国である。 Rocq（旧 Coq）は INRIA が開発し、Mistral AI には主要な研究者が集まり、大学教育でも証明支援系が使われている
   
• ポーランドは、Mizar を生んだ国であり、いまもこの分野の中核にいる。 Thor の著者８名のうち４名がポーランド系であり、AlphaProof にもポーランド出身の研究者が貢献している
   
• ドイツは、Isabelle と sledgehammer と Archive of Formal Proofs を生んだ。 本連載で扱った研究の多くが、その土台の上で動いている

何が争われているのか

• そして、この分野には根本的な対立がある。「そもそも形式言語へ翻訳する必要があるのか」という問いである
   
• 2025年のIMOでは、４つのシステムが金メダル相当を達成したが、そのうちの２つは形式言語、別の２つは自然言語で解答した。 DeepMind 自身が、2024年の形式化から2025年の自然言語へ方針を変えている
   
• 形式化の代償は、証明の長さである。 Seed-Prover の IMO 2025 第1問の Lean 証明は 4,357行であり、非形式的な対応物の16倍
   
• 一方で、形式化がなければ、AIのハルシネーションを見抜けない。 そしてAIが速くなるほど、人間による検証の費用は比例して増大する

第１部 ── まず、言葉を揃えます

本記事には、過去に公開済みの記事（タクティクスタイル）と過去に公開済みの記事（宣言的スタイル）に登場しなかった用語が出てきます。

先に、それらを説明します。

Neural Theorem Proving（ニューラル定理証明）

（深層）ニューラルネットワークを使って定理証明を行う研究を、こう呼びます。

日本語の訳語は、まだ定まっていないようです。

本記事では、「ニューラル定理証明」と書きますが、略して NTP と表記されることもあります。

この名前が使われ始めたのは、ごく最近のことです。

たとえば2026年6月の論文には、次のような書き方が現れます。

Neural theorem proving predates current LLM provers: GamePad studied Coq proof-state learning, TacticToe learned tactic search in HOL4, HOList and DeepHOL framed higher-order theorem proving as reinforcement learning, and CoqGym provided a large Coq dataset with AST-based tactic generation.

（筆者による日本語訳）

ニューラル定理証明は、現在の LLM による証明器より前から存在する。GamePad は Coq の証明状態の学習を研究し、TacticToe は HOL4 におけるタクティクの探索を学習し、HOList と DeepHOL は高階の定理証明を強化学習として定式化し、CoqGym は抽象構文木に基づくタクティク生成のための大規模な Coq のデータ集合を提供した。

出典
"TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics", arXiv:2606.09450, 2026年

この分野を調べるときは、*Neural Theorem Proving（Prover） という固有名詞を使ってください。

「AI 定理証明」で検索するより、はるかに的確に絞り込めます。

さきほど引用した文に登場した言葉について、補足説明いたします。

強化学習（reinforcement learning）とは、試行錯誤を通じて学ぶ手法です。行動を選び、その結果が良ければ報われ、悪ければ報われない。その繰り返しで、良い行動を選べるようにしていきます。囲碁や将棋のAIで使われた手法として知られています。

抽象構文木（abstract syntax tree、AST）とは、プログラムの構造を木の形で表したものです。文字の並びとしてではなく、「この式はこの部分から成る」という組み立てとして扱えます。

高階（higher-order）とは、関数そのものを引数にとったり、返したりできる仕組みのことです。Python の map や sorted(key=...) が、その例にあたります。

autoformalization（自動形式化）

日常の言葉で書かれた数学を、形式言語へ翻訳することです。

たとえば、「素数は無限に存在する」という日本語の文を、Lean や Isabelle が読める形に書き換える。その作業を自動化する研究を指します。

注意していただきたいのは、この作業が証明を書くこととは別だという点です。

まず主張を形式化し、次にその証明を書くという、２つの段階に分かれています。

そして、この分野では「形式化の質が、証明全体の成否を左右する」という指摘があります。
主張の書き方が悪ければ、その先へ進めないからです。

premise selection（前提選択）

巨大なライブラリの中から、使えそうな定理を選び出すことです。Lean の Mathlib には数十万の定理が登録されており、その中から、いま必要なものを見つけ出さなければなりません。

これは本質的に検索の問題であり、この分野の中心的な難所の一つとされています。

過去に公開済みの記事で紹介した Isabelle の sledgehammer も、この作業を担う仕組みです。

benchmark（ベンチマーク、問題集）

AIの性能を測るための共通の問題集です。

主なものを、次に挙げます。

名前	内容	問題数
miniF2F	高校の数学オリンピック（AMC、AIME、IMO）などから採った問題	488問
ProofNet	大学の学部レベルの教科書の演習問題	371問
PutnamBench	パトナム数学競技会の問題	1,697問
FIMO	IMO の候補問題	149問

上記の中で、miniF2F が最も広く使われています。

そして重要な特徴があります。

miniF2F は、Lean、Isabelle、HOL Light、Metamath の４つの言語 で同じ問題を用意しています。 そのため、言語をまたいだ比較ができます。

pass rate と pass@k

いずれも、正答率の測り方を表す語です。

pass rate は、そのまま「解けた問題の割合」を指します。

これに対して pass@k は、「k 回試して、１回でも解ければ正解」という測り方です。
たとえば pass@1 なら一発勝負、pass@64 なら64回まで試せることになります。

この違いは重要です。

試行回数が多ければ、当然ながら正答率は上がります。論文の数値を比べるときは、この条件を必ず確認してください。

本記事でも、条件が分かる場合は明記します。

expert iteration（専門家反復）

AIが解けた証明を、学習データに戻す手法です。

手順は、次のようになります。

1. AIに問題を解かせる
2. 解けたものだけを選ぶ
3. それを学習データに加えて、再び学習させる
4. １に戻る

この繰り返しによって、少ない元データから学習を進めていきます。

この分野では学習データの不足が最大の制約であったため、この手法が広く使われるようになりました。

step-level と whole-proof

先ほど触れた、２つの生成方式です。

step-level（一手ずつ）

処理系の現在の状態を入力し、次のタクティク１つを出力します。

出力を処理系に渡し、返ってきた新しい状態を、また入力する。

その繰り返しです。

利点は、処理系と密に対話できることです。
一手ごとに検査されるため、誤りが早い段階で分かります。

難点は２つあります。

完全な証明を組み立てるには外側の仕組みが必要であり、そして一手ごとに区切るため、証明全体を見渡した推論がしにくくなります。

whole-proof（丸ごと）

定理の主張だけを入力し、証明全体を一度に出力します。

利点は、証明全体を見渡した推論ができることです。

難点は、処理系との対話がないことです。 書き終えてから、まとめて検査されることになります。

この２つの対比は、過去に公開済みの記事で見たタクティクスタイルと宣言的スタイルの対比と、よく似ています。

Seed-Prover の論文には、次の記述があります。

Step-level provers incrementally generate Lean code line-by-line. While this enables close interaction with the Lean environment, it requires special scaffolding to generate a complete Lean proof, and the interaction is often too granular to allow high-level reasoning.

In contrast, whole-proof models generate an entire Lean proof at once, but typically lack interaction with the Lean compiler.

（筆者による日本語訳）

一手ずつ生成する証明器は、Lean のコードを一行ずつ増やしていく。

これにより Lean の環境と密に対話できるが、完全な Lean の証明を生成するには特別な足場が必要であり、対話の粒度が細かすぎて高い水準の推論ができないことが多い。

対照的に、証明を丸ごと生成するモデルは Lean の証明全体を一度に出力するが、Lean のコンパイラとの対話を欠くのが通例である。

出典
"Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving", arXiv:2507.23726, 2025年

補題、部分目標、Proof sketch について

証明の一部分を指す言葉を、３つまとめて説明いたします。

補題（lemma）とは、本題を証明するために、途中で用意する小さな定理のことです。

大きな定理を一度に証明できないとき、まず補題を証明し、それを使って本題へ進みます。

過去に公開済みの記事で扱った have は、この補題を書き記すための語でした。

部分目標（subgoal）とは、いま証明すべきことを分割したときの、一つ一つです。

「$A$ かつ $B$ を示せ」という目標は、「$A$ を示せ」と「$B$ を示せ」という２つの部分目標に分かれます。過去に公開済みの記事で見た 1 subgoal 2 subgoals という表示が、これです。

証明の素描（proof sketch）とは、証明の骨組みだけを書き、細部の根拠を省いたものです。

「何を仮定し、何を導き、何を示すか」は書かれていますが、各段階の根拠は書かれていません。 過去に公開済みの記事で扱った sorry を使えば、この状態のまま処理系に読ませられます。

用語のまとめ

用語	意味
Neural Theorem Proving（NTP）	ニューラルネットワークを使った定理証明の研究分野
autoformalization	日常の数学を、形式言語へ翻訳すること
premise selection	巨大なライブラリから、使える定理を選び出すこと
benchmark	性能を測るための共通の問題集
pass@k	k 回試して１回でも解ければ正解、という測り方
expert iteration	解けた証明を学習データに戻す手法
step-level generation	一手ずつタクティクを生成する方式
whole-proof generation	証明を丸ごと一度に生成する方式
補題（lemma）	本題を証明するために、途中で用意する小さな定理
部分目標（subgoal）	いま証明すべきことを分割したときの、一つ一つ
証明の素描（proof sketch）	証明の骨組みだけを書き、細部の根拠を省いたもの
合成データ（synthetic data）	人間ではなく機械が生成した学習データ
自己対戦（self-play）	モデルが自分で問題を作り、自分で解く仕組み
強化学習（reinforcement learning）	試行錯誤を通じて学ぶ手法。この分野では検査を通ったかどうかが報酬になる

---

第２部 ── 前史： 1997年から2020年

この分野は、LLM の登場とともに始まったわけではありません。
その前史から、順に追っていきます。

1997年 ── 骨格を書いて、隙間を埋めるという発想

過去に公開済みの記事で扱った Don Syme の Declare です。

証明の骨組みだけを書き、細部は自動証明の仕組みに任せる。
その発想が、このとき示されました。

当時、LLM は存在しません。
あくまで、人間が証明を書くための手法として提案されたものです。

しかしこの発想が、25年後に、まったく別の文脈で使われることになります。

2016年 ── 前提選択に、深層学習を使う

DeepMath という研究が発表されました。

巨大なライブラリから使えそうな定理を選び出す。

その作業に、ニューラルネットワークを使うという試みです。

ただし、この時点では証明そのものを生成してはいません。

あくまで、探索を助けるための部品にとどまっていました。

2018年から2019年 ── 環境とデータ集合が作られた

AIに定理証明を学ばせるには、学習の材料が要ります。

2018年から2019年にかけて、学習素材が整備されました。

名前	対象	内容
GamePad	Coq	証明状態の学習
TacticToe	HOL4	タクティクの探索を学習
HOList / DeepHOL	HOL Light	高階の定理証明を強化学習として定式化
CoqGym	Coq	抽象構文木に基づくタクティク生成のための大規模なデータ集合

この段階では、まだ Transformer は使われていません。

2020年 ── GPT-f

2020年に転機が訪れます。

Stanislas Polu と Ilya Sutskever（当時 OpenAI）が、GPT-f という仕組みを発表しました。

論文名
"Generative Language Modeling for Automated Theorem Proving"（arXiv:2009.03393）

この研究では、Transformer を、人間が書いた証明で学習 させました。

そして、Metamath という処理系 で、証明の一手を生成させた のです。

探索の方法は、最良優先探索（best-first search）です。
生成した候補のうち、最も見込みのあるものから試していきます。

この研究が示したのは、次のことでした。

言語モデルで、形式証明の一手を生成できる。

そして、これが現在まで続く系譜の出発点になりました。

GPT-f の入力・出力・学習データ

• 入力 ── Metamath の「ゴール」、つまり、いま示すべき主張です。文字列として与えられます。

• 出力 ── 「証明の一手」（proofstep）。具体的には、適用すべき定理と、その定理の変数に何を代入するかの組です。

論文にはその対応が明記されています。

The proofstep objective we use for training is a conditional language modeling objective that is asked to generate the PROOFSTEP given a GOAL, which is directly applicable to proof searches.

（筆者による日本語訳）

学習に用いる proofstep の目的関数は、GOAL が与えられたときに PROOFSTEP を生成するよう求める、条件付きの言語モデリングの目的関数である。これは証明の探索に直接適用できる。

学習データ ── ３段階に分かれています。

第１段階（事前学習） ── Common Crawl、arXiv、GitHub、Mathematics Stack Exchange などのウェブのデータ。

第２段階（微調整） ── Metamath の set.mm ライブラリ。人間が書いた証明の集まりです。約37,000の定理から、およそ300万の証明の一手が取り出されました。

第３段階（専門家反復） ── モデル自身が見つけた証明を、学習データに戻します。

規模 ── 最大のモデルで7億7,400万パラメータ、36層。

そして、注目すべき成果があります。

23個の短縮された証明が、Metamath の公式ライブラリに採用されました。

深層学習に基づくシステムの証明が、形式数学の共同体に受け入れられた最初の事例とされています。

出典
Stanislas Polu, Ilya Sutskever, "Generative Language Modeling for Automated Theorem Proving", arXiv:2009.03393, 2020年

第３部 ── 物差しが作られた： 2021年

何かを比べるには、共通の物差しが要ります。
2021年、*Neural Theorem Proving 研究に、その物差しが誕生しました。

miniF2F

Kunhao Zheng、Jesse Michael Han、Stanislas Polu による研究です。

論文名
"miniF2F: a cross-system benchmark for formal Olympiad-level mathematics"

中身は、488問の数学の問題です。
AMC、AIME、IMO といった高校の数学オリンピック、そして高校と大学の教科書から採られています。

同じ問題が、複数の言語で用意されています。

Lean、Metamath、Isabelle は、それぞれ488問すべてが揃っています。

HOL Light は、試験用165問と検証用165問の計330問で、部分的な対応にとどまっています。

出典
openai/miniF2F（公式リポジトリの統計）

そして488問は、244問ずつ、２つの組に分けられています。

**片方は「検証用」**です。手法を改良する途中で、性能を確かめるために使います。

**もう片方は「試験用」**です。
改良が終わった後、最終的な成績を測るために使います。

分ける理由は、公平さのためです。
改良に使った問題で成績を測れば、その問題に合わせて調整しただけかもしれません。一度も見ていない問題で測るからこそ、本当の実力が分かります。

論文が報告する成績は、通常この試験用の244問に対するものです。

同じ問題を複数の言語で用意したことで、言語をまたいだ比較ができるようになりました。

なお、この問題集には、後から誤りが見つかった主張も含まれていました。
そのため、それらを修正した版が作られ、近年の研究はそちらを使うことが増えています。

同じ「miniF2F での成績」と書かれていても、どの版で測ったのかによって、数値の意味が変わります。

論文には、この意図が明記されています。

We intend for miniF2F to be a community-driven effort and hope that our benchmark will help spur advances in neural theorem proving.

（筆者による日本語訳）

私たちは miniF2F を、共同体が主導する取り組みとしたいと考えている。そしてこのベンチマークが、ニューラル定理証明の進展を促す助けとなることを願っている。

出典
"miniF2F: a cross-system benchmark for formal Olympiad-level mathematics", ICLR 2022

この時点での成績は、次のとおりです。

仕組み	代数	数論
GPT-f（Lean）	51.4%	41.7%
GPT-3	6.0%	3.9%

出典
"miniF2F: a cross-system benchmark for formal Olympiad-level mathematics", ICLR 2022

ここで、注意していただきたいことがあります。

この比較は、同じ問題を解いているようで、条件が違うのです。

GPT-f は形式言語で証明を書き、処理系が検査します。 GPT-3 は日常の言葉で答えを出し、正解と照合されます。

それでも当時、この差は大きなものと受け止められました。

形式言語で書かせ、処理系に検査させる。

その方針の正しさを示す数字として読まれたのです。

LISA ── Isabelle の証明を学ぶ

2021年、Isabelle を対象とした研究も現れました。

Albert Qiaochu Jiang、Wenda Li、Jesse Michael Han、Yuhuai Wu による LISA（Language models of ISAbelle proofs）です。

この研究者たちの名前は、以降も繰り返し登場します。

本連載の第３回の記事の第11部で改めて扱います。

PACT ── 証明の副産物を学ぶ

Proof Artifact Co-training という手法も発表されました。

証明を書く過程で生まれる中間的な情報を、学習に使うという発想です。

この年の miniF2F での成績は29.6%（837Mのモデル）でした。

第４部 ── 骨格を書いて隙間を埋める： 2022年

この年、連載の主題と直結する研究が現れます。

Thor ── ハンマーを振るう

Albert Qiaochu Jiang らによる研究です。

論文名:
"Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers"（NeurIPS 2022）

この研究は、言語モデルを、既存の自動証明の仕組みと統合しました。

過去に公開済みの記事で紹介した Isabelle の sledgehammer を、思い出してください。外部の自動証明器に問い合わせ、証明の候補を探させる仕組みでした。

Thor は、言語モデルに「ここで sledgehammer を呼ぶべきか」を判断させます。

論文の要旨には、こうあります。

巨大なライブラリから有用な前提を選び出すという困難を克服するために、言語モデルと自動証明器を統合する枠組みを導入した、と。

Thor の入力・出力・学習データ

• 入力 ── Isabelle の証明状態。

• 出力 ── 次に書くべき証明の一手。 ただし、「ここで sledgehammer を呼ぶべきか」という判断も含みます。

• 学習データ ── Isabelle の Archive of Formal Proofs。人間が書き溜めた証明の集まりです。

HyperTree Proof Search ── 木を探索する

Guillaume Lample ら（当時 Meta AI）による研究です。

AlphaZero のような、対局を通じた学習の考え方を、定理証明に持ち込みました。

証明の探索を、木の探索として扱います。 そして探索の結果を学習に戻す。

Metamath と、Lean 版の miniF2F の両方で、強い成績を示しました。

Draft, Sketch, and Prove ── そして1997年へ

この年、最も重要な研究です。

著者
Albert Q. Jiang、Sean Welleck、Jin Peng Zhou、Timothée Lacroix、Jiacheng Liu、Wenda Li、Mateja Jamnik、Guillaume Lample、Yuhuai Wu

論文名
"Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs"（ICLR 2023）

題名が、そのまま手法を表しています。

「下書きし、素描し、証明する」

３つの段階があります。

1. Draft（下書き） ── LLM が、日常の言葉で証明の下書きを書く
2. Sketch（素描） ── その下書きを、形式言語の骨格へ変換する
3. Prove（証明） ── 残った隙間を、自動証明の仕組みが埋める

この手法の根拠として、論文が引用しているのが、1997年の Don Syme です。

論文の付録には、次の記述があります。

Interactive theorem provers such as Isabelle and Mizar use a declarative proof style (Syme, 1997), in which a proof is interleaved with conjectures and their corresponding proofs.

Syme (1997) stated that the list of conjectures in a declarative proof should be analogous to a proof sketch found in a mathematical textbook and sufficiently convincing for the reader.

（筆者による日本語訳）

Isabelle や Mizar のような対話型定理証明系は、宣言的な証明スタイル（Syme, 1997）を使う。

そこでは証明が、予想とそれに対応する証明とで織り合わされる。Syme（1997）は、宣言的な証明における予想の一覧は、数学の教科書に見られる証明の素描と類似したものであるべきで、読者を十分に納得させるものであるべきだと述べた。

文章はさらに続きます。

In practice, ITP users often prove a theorem by writing down a list of conjectures (a "formal sketch"), then attempt to find a proof of each conjecture (fill a "gap") with an automated system.

（筆者による日本語訳）

実際には、対話型定理証明系の利用者は、予想の一覧（「形式的な素描」）を書き下ろし、次に各予想の証明を自動のシステムで見つける（「隙間を埋める」）ことによって、定理を証明することが多い。

出典:"Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs", ICLR 2023, 付録A

つまり、こういうことです。

「骨格を書いて、隙間を自動で埋める」という手法は、LLMのために考案されたものではありません。

1997年に、人間が証明を書くための手法として 提案されていました。

そして、LLMは、その手法にたまたま適していた のです。

Draft, Sketch, and Prove の入力・出力・学習データ

• 入力 ── 日常の言葉で書かれた数学の問題です。

• 出力 ── ３段階で変化します。

1. 日常の言葉による証明の下書き
    
2. Isar の骨格（assume、have、show を並べたもの。細部は空欄）
    
3. sledgehammer が空欄を埋めた、完全な証明

学習データ ── 専用の学習を行っていません。

既存の大規模言語モデルを、そのまま使いました。

手法の側で工夫することで、汎用のモデルでも形式証明が書けることを示したのです。

第５部 ── 誰でも試せるようになった： 2023年

2022年までの研究には、共通の問題がありました。

他の研究者が再現できないのです。

コードが公開されていない。データも公開されていない。

そのうえ、膨大な計算資源を必要とする。

2023年、その状況が変わります。

LeanDojo ── 開かれた環境

LeanDojo は、Lean を使った定理証明のための、公開された基盤です。

カリフォルニア工科大学、NVIDIA、マサチューセッツ工科大学、カリフォルニア大学サンタバーバラ校、テキサス大学オースティン校という、５つの機関の研究者たちによる共同の仕事にあたります。

LeanDojo には、できることが ２つ あります。

1. 学習データの抽出 ── Mathlib から、証明のコードを取り出すこと
    
2. Python から Lean を動かすこと ── コードで Lean に指示を送り、証明の状態を受け取ること

LeanDojo は、Lean と対話できる最初の仕組みとして位置づけられています。

この LeanDojo と併せて、ReProver ── 検索を組み合わせた証明器 ―― も、同時に公開 されました。

ReProverは、前提選択を、検索の問題として扱うものです。

ReProver ：入出力データ および 学習データ

• 入力データ ── Lean の証明状態。

• 出力データ ── 次のタクティク。

• 学習データ ── Mathlib から抽出した証明。

Mathlib に蓄積された証明を、学習に使える形に変えるコードも公開されました。

その結果、学習データを、誰もが手元で作ることができるようになったのです。

Baldur ── 証明を修復する

Emily First、Markus N. Rabe、Talia Ringer、Yuriy Brun による研究です。

論文名:"Baldur: Whole-Proof Generation and Repair with Large Language Models"

２つのことをしました。

第１に、証明を丸ごと生成しました。 一手ずつではなく、全体を一度に。

第２に、失敗した証明を修復しました。

ここが重要です。 モデルに、前回の失敗した証明と、そのときのエラーメッセージを渡す。すると、証明を直せるのです。

評価は、Isabelle/HOL の6,336個の定理で行われました。

成績 ── Baldur 単独で、従来の最高であった Thor より 8.7%多くの定理を自動証明。 そして Thor と組み合わせると、65.7%の定理を完全に自動で証明できました。

出典
Emily First, Markus N. Rabe, Talia Ringer, Yuriy Brun, "Baldur: Whole-Proof Generation and Repair with Large Language Models", ESEC/FSE 2023

この数字は、数学の問題集ではなく、実際の証明の集まりに対するものです。

miniF2F の数値と、直接は比べられません。 対象が違うためです。

Baldur：入出力データ および 学習データ

• 入力 ── ２通りあります。

• 証明を生成するとき ── 定理の主張。

• 証明を修復するとき ── 前回の失敗した証明と、そのときのエラーメッセージ。

• 出力 ── Isabelle の証明全体。

• 学習データ ── Isabelle/HOL の6,336個の定理を含む、実際の証明の集まり。Archive of Formal Proofs から採られています。

Magnushammer ── 前提選択に Transformer を

Maciej Mikula らによる研究です。

sledgehammer が担っていた前提選択の作業を、Transformer で置き換えるという試みです。

Llemma ── 数学に特化した公開モデル

Zhangir Azerbayev、Hailey Schoelkopf らによる研究です。

数学のデータで学習させた、重みが公開されたモデルです。

この年、研究の土台が整いました。

第６部 ── 数値が跳ね上がった:2024年から2025年

この２年間で、成績が急激に伸びることになります。

2024年7月 ── AlphaProof と AlphaGeometry 2 が IMO で銀メダル相当

Google DeepMind が挙げた成果です。

国際数学オリンピック（IMO） の６問のうち、４問を解きました。

ここで、２つのシステムが登場します。

AlphaProof は、Lean のコードを書くAI です。

定理証明支援系そのものではありません。
Lean や Isabelle のような処理系とは、役割が違います。

AlphaProof が行うのは、以下の動作です。

1. 問題を受け取り、Lean のコードで証明を書く
2. 生成したコードを、Lean に検査させる
3. Leanの検査に合格しなければ、再度 書き直して再び検査に臨む

この動作はつまり、本記事の第１部で扱った whole-proof generation にあたります。

AIが証明を生成 し、Leanなどの定理証明支援処理系が検査 する。

その組み合わせです。

Lean の検査 を合格した証明は、正しいことが数学的に保証されます。
AIが誤った推論をしていれば、Leanが確実に弾いてくれる（不合格にする）のです。

定理証明支援系にチェックを仰がない場合、
大規模言語モデルが数学の問題を解いた結果は、正しいかどうかを人間が肉眼で見て、確かめる必要があります。

AlphaProof には、その必要がありません。その役割は、定理証明支援系（Lean 4）が担ってくれるからです

以上が、AlphaProof です。

これがひとつめのAIです。

次に登場するふたつ目のAIは、AlphaGeometry です。

AlphaGeometry 2 は、幾何の問題に特化した別のシステムです。
2024年1月に発表された AlphaGeometry の改良版 にあたります。

なぜ、幾何だけ別のシステムなのでしょうか。

Natureに掲載された論文 には、その理由が記されています。

原文

Given specific Mathlib library limitations for Olympiad-style geometry ('IMO-style geometry' in Methods), the geometry problem (P4) was addressed using the specialized AlphaGeometry 2 system.

（筆者による日本語訳）

オリンピック形式の幾何に対する Mathlib ライブラリ固有の制約を踏まえ、幾何の問題（第4問）は、専用の AlphaGeometry 2 システムを用いて扱われた。

出典:Thomas Hubert ほか（Google DeepMind）, "Olympiad-level formal mathematical reasoning with reinforcement learning", Nature, 2025年11月12日

Mathlib とは、Lean の数学ライブラリです。

人間の数学者たちが積み上げてきた、数十万の定理の集まり です。

AlphaProof が証明を書けるのは、この Mathlib があるから です。
すでに証明された定理を呼び出しながら、新しい証明を組み立てます。

そして、ここに落とし穴がありました。

Mathlib の幾何は、現代数学の流儀で作られています。

たとえば「点」や「直線」を、ベクトル空間やアフィン空間といった抽象的な枠組みの上で定義 します。
大学の学部と大学院で教わる数学では、これが標準です。

しかし、数学オリンピックの幾何は違います。

「三角形の内心」「円に内接する四角形」「角の二等分線」といった、初等幾何の言葉　で問題が書かれます。紙に図を描いて考える、あの幾何です。

初等幾何とは、中学と高校で習う図形の幾何 のことです。

三角形、円、平行線、合同、相似。
補助線を引いて、角度が等しいことを示す。

あの世界です。

紀元前３世紀のユークリッドが体系化した形から、本質的には変わっていません。

この２つは、同じ「幾何」でも、扱う枠組みが違います。

オリンピックの幾何を Mathlib で書こうとすると、初等的な概念を抽象的な定義から組み立て直す作業が必要になります。

そして、その作業に必要な定理が、Mathlib には十分に揃っていませんでした。

そこで DeepMind は、幾何の問題だけを AlphaProof に扱わせず、別のシステムに任せる判断を下しました。

AlphaGeometry 2 は、Lean を使わずに、初等幾何に特化した独自の仕組みで、幾何の問題を扱う選択をしたのです。

この判断が、本記事の第７部とつながります。

第７部では、「Lean と Isabelle の成績の差は、ライブラリの規模と問題集の性質による」という話をします。

ここでも同じことが起きています。

AIの能力ではなく、ライブラリに何が揃っているかが、扱えることを決めているのです。

その結果として、AlphaProof が代数の第1問、数論の第2問、そして代数の第6問を解き、AlphaGeometry 2 が幾何の第4問を解きました。

IMO とは、どういう競技か を補足します。

100を超える国から、各国６名の高校生が参加します。
２日間にわたり、１日４時間半で３問を解きます。１問7点、合計42点。

全問完答する参加者は、通常１%未満とされています。

その競技で、AIが銀メダル相当の成績を収めました。

この方法論は、2025年11月12日に Nature 誌に発表されました。

出典:AI achieves silver-medal standard solving International Mathematical Olympiad problems, Google DeepMind

実際の問題文を見てみる

AIが解いた問題のうち、２つを実際に示します。

第１問（代数、最も易しい問題）

すべての正の整数 $n$ について、次の整数が $n$ で割り切れるような実数 $\alpha$ を、すべて求めよ。

$$\lfloor \alpha \rfloor + \lfloor 2\alpha \rfloor + \cdots + \lfloor n\alpha \rfloor$$

記号の説明をします。

$\lfloor x \rfloor$ は床関数（floor function）と呼ばれ、$x$ 以下の最大の整数を表します。$\lfloor 3.7 \rfloor = 3$、$\lfloor 5 \rfloor = 5$ です。Python の math.floor() と同じものです。

つまり、問われている問題は以下になります。

$\alpha$ を1倍、2倍、…、$n$ 倍して、それぞれ小数点以下を切り捨てる。
その総和が、どんな $n$ についても $n$ で割り切れる。
そのような $\alpha$ は何か。

答えは「偶数の整数すべて」 です。

これが、その年の IMO で 最も易しい問題 でした。

第６問（代数、最も難しい問題）

$\mathbb{Q}$ を有理数全体の集合とする。

関数 $f: \mathbb{Q} \to \mathbb{Q}$ が aquaesulian であるとは、すべての有理数 $x, y$ について、次の少なくとも一方が成り立つことをいう。

$$f(x + f(y)) = f(x) + y \quad \text{または} \quad f(f(x) + y) = x + f(y)$$

このとき、次を示せ。ある整数 $c$ が存在して、どんな aquaesulian な関数 $f$ についても、$f(r) + f(-r)$ の形で表される有理数は高々 $c$ 種類しかない。

そして、そのような $c$ の最小値を求めよ。

「aquaesulian」という語は、この問題のために作られた造語です。

2024年の IMO は、イギリスのバースで開かれました。
その町のローマ時代の名が Aquae Sulis（「スリスの水」の意）だったことにちなんでいます。

答えは $c = 2$ です。

この問題の難しさは、２段階になっています。

第１段階 ── 「高々2種類しかない」ことを証明する。

第２段階 ── 「ちょうど2種類になる関数が、実際に存在する」ことを示す。

そして第２段階では、そのような関数を具体的に構成しなければなりません。

公式の解答では、$f(x) = \lfloor x \rfloor - {x}$ という関数が使われています。ここで ${x} = x - \lfloor x \rfloor$ は小数部分です。

この関数を思いつくことが、極めて困難でした。

なぜ、第６問が特別だったのか

509人の参加者のうち、完答できたのは５人だけです。

そして、AlphaProof はこれを解きました。

AlphaProof が生成した証明

実際に生成されたコードを、ご覧ください。

open Polynomial

theorem imo_2024_p6
    (IsAquaesulian : (ℚ → ℚ) → Prop)
    (IsAquaesulian_def : ∀ f, IsAquaesulian f ↔
      ∀ x y, f (x + f y) = f x + y ∨ f (f x + y) = x + f y) :
    IsLeast {(c : ℤ) | ∀ f, IsAquaesulian f → {(f r + f (-r)) | (r : ℚ)}.Finite ∧
      {(f r + f (-r)) | (r : ℚ)}.ncard ≤ c} 2 := by
  exists@?_
  · useλu b=>if j:u 0=0then by_contra λc=>?_ else ?_
    · suffices:({J|∃k,u k+u (-k)= J}) ⊆{0}
      · simp_all[this.antisymm]
      rintro - ⟨a, rfl⟩
      contrapose! c
      simp_all
      suffices:{U|∃examples6, (u) ‹ℚ› +u ( -‹_›)= U} ⊆{0,(u (a : Rat)+ (u<|@@↑(( (-a ))))) } ..
      · use ( Set.toFinite ( _) ).subset ↑@@this , (Set.ncard_le_ncard$ (((this )) ) ).trans (Set.ncard_pair$ Ne.symm (↑ ( (c)) ) ).le
      rintro-⟨hz, rfl⟩
      induction b @hz a
      · have:=b (-a)$ hz+u a
        have:=b hz hz
        simp_all[add_comm]
        have:=b (-hz) (hz+u ↑(hz))
        simp_all[ add_assoc, C]
        induction this
        · simp_all
          have:=b hz (hz+(u a+u (-a)))
          have:=b (hz+(u a+u (-a)))$ hz+(u a+u (-a))
          use .inr$ by_contra$ by hint
        have:=b hz$ hz+(u hz+u (-hz))
        cases b (hz+(u hz+u (-hz)))$ hz+(u hz+u (-hz))with|_=>hint
      have:=b (-hz) (u hz+a)
      have:=b$ -a
      specialize this (u hz+a)
      simp_all[ ←add_assoc]
      have:=b 0
      have:=b
      specialize b a a
      simp_all[add_comm]
      have:=(this<| -a) (↑a + (((u a))): (↑_ :((( _) ) ) )) ..
      simp_all[add_assoc]
      cases this
      · simp_all
        contrapose! IsAquaesulian_def
        simp_all
        exfalso
        have:=this a (a+(u hz+u ( -hz)))
        simp_all[Ne.symm,Bool]
        have:=‹∀congr_arg G,_› (a+(u hz+u (-hz)))$ a+(u ↑hz+u ↑( -hz) )
        simp_all
      have:=this a (a +(u a+u (-a)))
      cases‹forall Jd S,_› (a+(u a+u (-a))) ( a + (u a +u ↑(-a)))with| _ =>hint
    simp_all
    cases b 0 0with|_=>exact absurd (b 0$ (0+(1 *(@(u ↑.((0) )))))^ 01: ↑ ((_)) ) (id$ (by(cases ( b (u 0) ( (u 0)))with|_ => continuity)))
  rintro K V
  specialize V $ λ N=>-N+2 *Int.ceil N
  specialize( V $ (IsAquaesulian_def _).mpr _)
  · simp_rw [ ←eq_sub_iff_add_eq']
    ring
    use mod_cast@?_
    norm_num[<-add_mul,Int.ceil_eq_iff]
    useλc K=>(em _).imp (⟨by linarith[Int.ceil_lt_add_one c,Int.le_ceil K],.⟩) (by repeat use by linarith[.,Int.le_ceil c,or,Int.ceil_lt_add_one$ K])
  simp_all[Int.ceil_neg, ←add_assoc]
  suffices:2<=V.1.toFinset.card
  · let M:=V.1.toFinset
    norm_num[this,V.2.trans',(Set.ext$ by simp_all[M] : {x :Rat|∃t:Rat, (↑2 ) * ( ⌈ t ⌉:(ℚ ) ) .. + (- (2 *⌊(t)⌋)) = ↑x} = M)]
  use Finset.one_lt_card.2$ by exists@0,V.1.mem_toFinset.2 (by exists-1),2,V.1.mem_toFinset.2 (by exists 1/2)

出典
IMO 2024 P6, Google DeepMind

このコードの読み方

DeepMind の公開ページをご覧になる方のために、読み方を説明します。

行数について

注釈を除いたコードは、69行です。

内訳は、定理の宣言部が7行、証明の本体が62行です。

ただし、この数字を他の証明と比べることはできません。

理由は、次の一行をご覧いただければ分かります。

use Finset.one_lt_card.2$ by exists@0,V.1.mem_toFinset.2 (by exists-1),2,V.1.mem_toFinset.2 (by exists 1/2)

AlphaProof は、複数のタクティクを１行に詰め込みます。
人間が読みやすく書けば、これは数行に分かれます。

公開ページの構成

DeepMind のページは、コードだけを載せているのではありません。

タクティクを１つ実行するごとに、その時点の証明状態を示す表が挿入されています。 何が仮定として使えるか、そして何を示すべきか。

過去に公開済みの記事で扱った Lean の Infoview を、思い出してください。あの表示が、各行に添えられているとお考えください。

さらに、英語の注釈が付いています。

-- If f(x) + f(-x) = 0 for all x, we are done. といった説明です。

この注釈は、AlphaProof が生成したものではありません。

Lean の専門家９名（Oliver Nash、Bhavik Mehta、Paul Lezeau ら）が、後から付けたものです。

変数名について

読みにくさの一因が、変数名です。

AlphaProof は、独自の命名をします。

問題文では関数を $f$、有理数を $x, y$ と書いていますが、コードでは u、hz、b といった名前が使われています。

第２問の解説を書いた Rishi Mehta 氏は、この点をこう述べています。

原文:

Note that in its infinite wisdom, AlphaProof decides to rename pairs $(a, b)$ to b, so that it must reference the elements as b.1 and b.2. It has also chosen, for reasons best known to itself, to rename the variable $g$ to Y.

（筆者による日本語訳）

**その底知れぬ知恵によって、AlphaProof は組 $(a, b)$ を b と改名することに決めた。

そのため、その要素を b.1 と b.2 として参照しなければならなくなっている。

また、それ自身にしか分からない理由で、変数 $g$ を Y に改名することも選んでいる。**

出典
AlphaProof's Greatest Hits, Rishi Mehta, 2024年11月17日

どこを見れば、証明の流れをつかめるか

コードの構造 は、大きく２つの部分 に分かれています。

前半（exists@?_ から cases b 0 0with|_=>... まで）── 「$f(r) + f(-r)$ の取りうる値は、高々２種類である」ことを証明しています。

後半（rintro K V から最後まで）── 「実際に２種類の値を取る関数が存在する」ことを示しています。

後半部分のコアとなる箇所 は、次の一行です。

specialize V $ λ N=>-N+2 *Int.ceil N

これは、$f(x) = -x + 2\lceil x \rceil$ という関数を提示している箇所です。

Int.ceil が天井関数、λ N=> が関数を作る記法です。

そして、最後の一行 で、２つの異なる値 を示しています。

use Finset.one_lt_card.2$ by exists@0,V.1.mem_toFinset.2 (by exists-1),2,V.1.mem_toFinset.2 (by exists 1/2)

by exists -1 で $r = -1$ を代入し、$f(-1) + f(1) = 0$ を得ます。

by exists 1/2 で $r = 1/2$ を代入し、$f(1/2) + f(-1/2) = 2$ を得ます。

$0$ と $2$。これが、求める２つの値です。

最後に表示されるもの

ページの末尾に、次の記述があります。

#print axioms imo_2024_p6
'imo_2024_p6' depends on axioms: [propext, Classical.choice, Quot.sound]

これは「この証明が、どの公理に依存しているか」を表示する命令と、その結果です。

公理とは、証明の出発点として無条件に認める前提のことです。

ここに並んでいる propext、Classical.choice、Quot.sound の３つは、いずれも Lean に標準で組み込まれている公理です。

つまり、この証明は特別な仮定を一切追加せずに成立しています。

もしも AlphaProof が sorry を使って証明の一部を未完のまま残していれば、上記の一覧リストには sorry も表示されていたはずです。

その表示がないということは、証明に未証明の箇所が存在しないということを意味しています。

以上が、 AlphaProof が 生成した証明 です。
そして、この証明は、Lean 4 によって正しい（成立する）ことが確認されました。

採点にあたったティモシー・ガワーズ（フィールズ賞受賞者であり、IMO の金メダリスト）が、次のように評しています。

原文:

The fact that the program can come up with a non-obvious construction like this is very impressive, and well beyond what I thought was state of the art.

筆者による日本語訳

このプログラムが、これほど自明でない構成を思いつけるという事実は、極めて印象的である。私が最先端だと思っていた水準を、はるかに超えている。

出典
AI achieves silver-medal standard solving International Mathematical Olympiad problems, Google DeepMind, 2024年7月25日

さらに、ガワーズ自身がこの問題を解こうと試みたものの、２つの異なる値を与える関数を見つけられなかったと報告されています。

出典
AlphaProof's Greatest Hits, Rishi Mehta, 2024年11月17日

解けた問題と、解けなかった問題

問題	分野	結果
第1問	代数	AlphaProof が解いた
第2問	数論	AlphaProof が解いた
第3問	組合せ論	解けなかった
第4問	幾何	AlphaGeometry 2 が解いた（19秒）
第5問	組合せ論	解けなかった
第6問	代数	AlphaProof が解いた

解けなかったのは、組合せ論の２問です。

対話篇： AlphaProofへの数学問題文の渡し方

タロウくん：
先生、一つ気になることがあります。

専任講師：
どうぞ。

タロウくん：
AlphaProof には、問題文がどう入力されたのでしょうか？
IMO の参加者は、印刷された問題用紙を受け取ります。英語の文章と数式が書かれた紙です。

専任講師：
そうですね。

タロウくん：
あの文章が、そのまま AlphaProof に入力されたのでしょうか？

専任講師：
いいえ。

タロウくん：
・・・違うのですか。

専任講師：
問題文は、人間の専門家が手作業で Lean の形式言語へと翻訳した上で、AlphaProofに入力されました。

Nature の論文には、こう記されています。

The remaining five non-geometry problems (algebra, P1 and P6; number theory, P2; combinatorics, P3 and P5) were manually formalized in Lean by experts immediately after the competition's release.

（筆者による日本語訳）

幾何以外の残り５問（代数の第1問と第6問、数論の第2問、組合せ論の第3問と第5問）は、競技の問題が公開された直後に、専門家によって手作業で Lean に 形式化 された。

出典
Thomas Hubert ほか（Google DeepMind）, "Olympiad-level formal mathematical reasoning with reinforcement learning", Nature, 2025年11月12日

タロウくん：
つまり、AIが問題として受け取ったのは、すでに Leanのコードに翻訳済みのコード文 だった、ということでしょうか？

専任講師：
そのとおりです。

先ほど眺めたコードを、思い出してください。

theorem imo_2024_p6
    (IsAquaesulian : (ℚ → ℚ) → Prop)
    (IsAquaesulian_def : ∀ f, IsAquaesulian f ↔
      ∀ x y, f (x + f y) = f x + y ∨ f (f x + y) = x + f y) :
    IsLeast {(c : ℤ) | ∀ f, IsAquaesulian f → {(f r + f (-r)) | (r : ℚ)}.Finite ∧
      {(f r + f (-r)) | (r : ℚ)}.ncard ≤ c} 2 := by

この := by までの部分 が、人間が書いた問題文 です。

そして := by より後が、AlphaProof が書いた（生成した）証明（コード） です。

タロウくん：
・・・しかし、先生・・・それでは条件が違うのではないでしょうか。

専任講師：
違います。

そして、その点は論文自身が認めています。

タロウくん：
どういうことですか？

専任講師：
「自動形式化」という研究があることを、第１部で扱いました。

日常の言葉で書かれた数学を、形式言語へ翻訳する研究 です。

AlphaProof は、その部分を自分では行わない のです。

タロウくん：
先ほどの説明だと、そこは、Leanのコードを書ける人間の専門家が（AlphaProofの）代わりに行ってくれていた、のですよね？

専任講師：
そうです。

別の論文が、この点を明確に指摘しています。

This two-step process and its limitations were evident even in AlphaProof's silver-medal performance at the 2024 IMO, where problem statements needed manual translation before automated proof synthesis.

（筆者による日本語訳）

この２段階の過程とその限界は、2024年のIMOで AlphaProofが銀メダル相当の成績をはじきだした場合においてすら、明らかであった。

そこでは、自動的な証明の合成に先立って、問題の主張を人手で翻訳する必要があったのである。

出典
Prithwish Jana ほか（ジョージア工科大学）, "ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings", arXiv:2510.15681

以上、2024年のIMO（国際数学オリンピック）における AlphaProofの功績を見てきました。

AlphaProof が獲得した得点は、28点（42点満点）でした。

金メダルの境界は29点だったので、惜しくも あと１点、金メダルには手が届きませんでした。

なお、この成績は、609人の参加者のうち、上位58位に相当する結果でした。

IMO のメダルについて

IMO（国際数学オリンピック） では、参加者のおよそ半数がメダルを受け取ります。

金、銀、銅の割合 は、おおむね1対2対3 と定められています。

2024年の場合、金メダルは609人中58人でした。約9.5%です。

つまり、AIが到達したのは金の境界のすぐ下という位置です。

なお、42点満点を取ったのは、609人中１人だけでした。

２年間の変化

そして翌2025年7月、Gemini Deep Think が金メダル相当の成績を収めています。OpenAI の仕組みも同等でした。

2023年には１問も解けなかったものが、2024年に銀、2025年に金。

２年間の変化です。

2025年 ── 公開されたモデルが相次ぐ

この年、重みが公開されたモデルが次々に発表されました。

モデル	開発	特徴
DeepSeek-Prover-V2	DeepSeek	Lean 4 向け。強化学習と自己対戦。公開モデルとして miniF2F の最高成績
Kimina-Prover	Numina と Kimi	強化学習による大規模な形式推論モデル
Goedel-Prover	プリンストン大学ほか	合成データによる学習
STP	スタンフォード大学	自己対戦。予想を立て、それを証明する繰り返し

上の表に登場する言葉について、説明させていただきます。

合成データ（synthetic data）とは、人間が書いたものではなく、機械が生成した学習データのことです。Neural Theorem Proving では、AIが解いた証明を学習データに戻す手法が広く使われています。

自己対戦（self-play）とは、モデルが自分で問題を作り、自分でそれを解く仕組みです。
囲碁のAIが自分と対局して強くなったのと、同じ発想です。

強化学習については、第１部で触れました。
試行錯誤を通じて学ぶ手法です。

Neural Theorem Proving では、「証明が定理証明処理系による検査を通ること（合格すること） が、報酬 になります。

DeepSeek-Prover-V2 の入力・出力・学習データ

入力 ── Lean 4 の定理の主張。

出力 ── have による骨格と、タクティクによる証明を組み合わせた Lean 4 のコード。 約60行になることもあります。

学習データの作り方が、特徴的です。

1. 大きなモデル（DeepSeek-V3）が、定理を高水準の証明の素描へ分解する
2. 同時に、その素描を Lean 4 で形式化し、部分目標の列にする
3. 小さな7Bのモデルが、各部分目標を証明する
4. 解けた証明を組み合わせて、完全な証明を作る
5. その完全な証明と、最初の素描を対にして、学習データにする

つまり、AIが自分で教材を作っています。

この手法は、本連載の第２回の記事の第９部で詳しく扱います。

出典:ZZ Ren ほか, "DeepSeek-Prover-V2", arXiv:2504.21801, 2025年

Kimina-Prover の入力・出力・学習データ

入力 ── Lean 4 の定理の主張。

出力 ── ここが特徴的です。

思考のブロックと、Lean のコードが、交互に織り込まれた形で出力されます。

論文は、この形式を formal reasoning pattern（形式的推論のパターン）と呼んでいます。

思考のブロックでは、モデルが日常の言葉で戦略を述べ、問題を分解し、途中の推論を素描します。その中に、部分的な Lean のコードが混じることもあります。

そして最後に、完全な Lean の証明が出力されます。

学習データ ── NuminaMath-LEAN。競技数学から採った10万件の Lean 4 の主張と証明の集まりです。

人間が注釈を付けた Lean 4 のコーパスとしては最大とされています。

基盤モデル ── Qwen2.5-72B。

学習の方法 ── Kimi k1.5 の強化学習の仕組み。報酬は単純です。生成した Lean のコードが検査を通れば1、通らなければ0。

注目すべき点 ── Lean のエラーメッセージを読み、修正を提案できます。 一から書き直すより、はるかに効率が良いと報告されています。

出典:

• Numina & Kimi Team, "Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning", arXiv:2504.11354, 2025年
• NuminaMath-LEAN, Hugging Face

Goedel-Prover の入力・出力・学習データ

• 入力 ── Lean 4 の定理の主張。

• 出力 ── have の列と、高水準のタクティクを組み合わせた Lean 4 のコード。 その実例は、本連載の第２回の記事の第９部でご覧いただきます。

• 学習データ ── 合成データ。既存の問題を形式化し、解けた証明を学習に戻す循環です。

• 基盤モデル ── 後の版では Qwen3 を使っています。

STP について、少し詳しく説明します。

Kefan Dong と Tengyu Ma による研究です。論文名:"STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving"

この分野の最大の制約は、学習データの不足でした。専門家が書いた形式証明は、大量には存在しません。

STP は、モデル自身に予想を立てさせます。
そして、その予想を証明させてみて、成功した証明を、学習データに戻します。

STP の入力・出力・学習データ

• 入力 ── ２通りあります。 予想を立てるときは、既に証明できた定理の集まり。証明するときは、生成された予想。

• 出力 ── これも２通り。 新しい予想と、その証明です。

• 学習データ ── 自分で生成したものを、そのまま使います。 成功した証明だけを選んで戻す循環です。

• 成績 ── Lean の LeanWorkbook において、累積の正答率が 26.3%。 従来の手法の約２倍です。

出典
Kefan Dong, Tengyu Ma, "STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving", arXiv:2502.00212, 2025年

なお、LeanWorkbook は、 miniF2F とは別の問題集です。
この26.3%という数値を、miniF2F の数値と並べて比べることはできません。

ここで注意していただきたいことがあります。

STP が生成する「予想」は、学習のための問題であって、数学的に新しい発見ではありません。

はじめにの対話で触れた論点と、混同しないようにしてください。

2025年 ── そして、学習し尽くされた

miniF2F の成績が、次のように推移しました。

時期	正答率	システム	モデルの規模
2021年2月	29.6%	Proof Artifact Co-training	837M
2023年10月	26.5%	ReProver	299M
2024年8月	30.7%	COPRA	──
2024年10月	33.6%	TheoremLlama	8B
2025年9月	99.2%	Hilbert	──
2025年	99.6%	Seed-Prover	──

出典
"From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier", arXiv:2607.07779, 2026年、表4

これは「最高記録の推移」ではありません。

元になったサーベイ論文の表は、モデルの規模や手法の違いを示すために、代表的なシステムを並べたものです。
そのため、同じ年に、この表より高い成績を出したシステムが存在します。

たとえば、2024年から2025年にかけて、DeepSeek-Prover は88.9%を記録しています。
表の33.6%と99.2%のあいだには、多数のシステムが並んでいます。

表を時系列に並べると、2024年10月の33.6%から2025年9月の99.2%へ、一気に跳ね上がったように見えます。
しかし実際には、その間に段階的な積み重ねがありました。

もう一つ、気づかれた方がいるかもしれません。

2021年の29.6%から、2023年には26.5%へ。数字が下がっているように見えます。

しかし、これは性能が落ちたのではありません。モデルの規模が違います。

2021年の Proof Artifact Co-training は837M、2023年の ReProver は299M。３分の１以下の規模で、近い成績を出しています。

この表は、「6年間で何が起きたか」の輪郭を示すものとして、ご覧ください。

Seed-Prover は ByteDance の Seed チームによるものです。

Seed-Prover の入力・出力・学習データ

入力 ── Lean 4 の定理の主張。

出力 ── Lean 4 の証明全体。

特徴 ── 本記事の第１部で扱った「一手ずつ生成する方式」と「丸ごと生成する方式」の両方の難点を、論文が指摘しています。

そのうえで、補題を中心に据えた反復の仕組みを採りました。

学習データ ── 詳細は公開されていません。

出典
"Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving", arXiv:2507.23726, 2025年

99.6%とは、試験用の244問のうち243問を解いたということです。

残る未解決は、2007年のIMO候補問題の代数の第6問、ただ１問です。

サーベイ論文には、次のように書かれています。

The benchmark has been effectively saturated by recent systems. This saturation—from approximately 30% in 2021 to near-100% in 2025, demonstrates remarkable progress but also highlights the need for more challenging benchmarks.

（筆者による日本語訳）

このベンチマークは、近年のシステムによって事実上、解き尽くされた。
2021年の約30%から2025年の100%近くへというこの到達は、目覚ましい進展を示すと同時に、より難しいベンチマークの必要性をも浮き彫りにしている。

出典
同上

同じサーベイ論文は、こうも述べています。

「３年前には手が届かないと思われた問題が、いまや確実に解かれる。しかし数学者が実際に取り組んでいる問題への隔たりは、依然として大きい」と。

この「隔たり」については、本連載の第４回の記事の第14部で改めて扱います。

第７部 ── Lean と Isabelle の差は、なぜ生まれたか

以下は、miniF2Fという問題集 に挑んだ結果の成績です。

言語	記録	システム
Lean	99.6%	Seed-Prover
Isabelle	66.0%	ProofAug

Lean と Isabelle のあいだには、大きな差があります。

なお、ここで注意すべきは、両者は条件を揃えて比べたものではないということです。
モデルの規模も、試行回数も、使った問題集の版も、両者で異なります。

それでも、この開きは無視できません。

同じ問題集を使いながら、なぜこれほど差がつくのでしょうか。

この差は、言語（ Lean と Isabelle ）の優劣を示しているのでしょうか。

言語の優劣に結び付くパフォーマンスの差ではありません。

HybridProver の論文が、両者のパフォーマンスが大きく開いた理由に言及しています。

More work uses LLMs for Lean and gets better results on miniF2F than for Isabelle, because Lean is mainly used for mathematics, with the largest math library, and miniF2F is a mathematical benchmark suite. In contrast, Isabelle users tend to focus more on system verification.

（筆者による日本語訳）

Lean を対象に LLM を使う研究のほうが多く、miniF2F での成績も Isabelle より良い。

それは、Lean が主に数学に使われ、最大の数学ライブラリを持ち、そして miniF2F が数学の問題集だからである。

対照的に、Isabelle の利用者はシステム検証により重きを置く傾向がある。

出典
"HybridProver", arXiv:2505.15740, 2025年

この論文は、以下も述べています。

In system verification, proofs of correctness vary significantly for different implementations.

（筆者による日本語訳）

システム検証においては、正しさの証明は実装ごとに大きく異なる。

差を生んでいる要因は、次の３つに整理できます。

第１ に、ライブラリの規模です。

Lean の Mathlib は、定理証明支援系の中で、最大の数学ライブラリ です。
学習データの量が違います。

第２ に、問題集の科目があります。

miniF2F は、数学の問題集 です。
数学に使われる言語のほうが、成績が良くなるのは当然です。

第３ に、利用者の関心の所在の違いです。

Isabelle のユーザ は、システム検証に重きを置きます。

過去に公開済みの記事で触れた seL4 の検証も、Isabelle で行われました。

そして、システム検証の証明は、実装ごとに大きく異なります。

数学の定理のように、共通の型に当てはめにくい のです。

評価の物差しが、言語の順位を決めている

ここに、注意すべき構造があります。

miniF2F は、数学 の問題集です。
当然、数学の定理証明問題に頻繁に使われる言語（定理証明支援系）のほうが、この問題集を解くのが得意です。

Isabelle の成績が低いのは、Isabelle が処理系それ自体が持つ性能として、Lean よりも劣っているからではありません。

取り組む対象の問題集が、Isabelle の主戦場ではない からです。

この点は、機械学習に携わる方には馴染みのある話だと思います。

取り組む問題の領域の選び方が、あるアルゴリズムや学習済みモデルのパフォーマンスの測定結果を左右する。
それと同じ構造です。

Isabelle 側の研究も、着実に進んでいます

数字を追ってみます。

年	正答率	システム	問い合わせ回数
2024年	56.1%	SubgoalXL	1問あたり16,384回
2025年	59.4%	HybridProver	──
2025年	66.0%	ProofAug	1問あたり2,100回

ProofAug に注目してください。

成績が上がっただけではありません。 問い合わせ回数が、８分の１以下になっています。

SubgoalXL が56.1%を達成するのに16,384回を要したのに対し、ProofAug は66.0%を2,100回で達成しました。

論文には、こう書かれています。

we achieve a cumulative pass rate of 66.0% after curation of the dataset (61.9% for the original version) with 2100 queries to the model per problem (In contrast, the previous SOTA in Isabelle, Subgoal-XL, only achieves 56.1% using 16384 queries per problem).

（筆者による日本語訳）

データ集合を整えた後、1問あたり2,100回の問い合わせで、累積の正答率66.0%を達成した（元の版では61.9%）。

対照的に、Isabelle におけるそれまでの最高記録である SubgoalXL は、1問あたり16,384回の問い合わせを使って56.1%にとどまっている。

出典
"ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis", ICML 2025

では、ProofAug は何をしたのでしょうか。

その答えが、次の第８部です。

第８部 ── 宣言的スタイルは、どう扱われているか

宣言的スタイル をめぐっては、４つの異なる方向性の研究が進行中です。

方向その１: 言語を作り変える ── MiniLang

2025年の研究です。

Isar の構文が多すぎることを、問題として指摘しました。

There are at least three problems: the abundance of expert-oriented features, extensive syntactic redundancy, and the substantial demand for proof automation in declarative proofs.

（筆者による日本語訳）

問題は少なくとも３つある。

専門家向けの機能の過多、広範な構文の冗長性、そして宣言的な証明における証明自動化への実質的な要求である。

出典:"A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL", 2025年

そこで、構文を減らした新しい言語 が設計されました。

MiniLang と名づけられた、Isabelle/HOL の上で使う証明言語です。

このMiniLangは、最初から大規模言語モデルを意識して設計されました。

学習すべき構文の種類が少ないほうが、大規模言語モデルにとって扱いやすいという考えです。

MiniLang は、AIではなく言語です

証明を書くのはAIで、MiniLang はそのAIが書くための言語です。

Isar の構文を減らせば、覚えるべきことが減り、大規模言語モデルは扱いやすくなります。

賢いモデルを作るのではなく、易しい言語を作る。 これが、この研究の選んだ道です。

過去に公開済みの記事で扱った1997年の Declare を、思い出してください。 Syme は「証明はタクティクによってではなく、わずか３つの構成子だけで記述される」と書きました。

構文を極限まで減らすという設計を、MiniLang が別の動機から再発見しています。

方向その２:　書き方を定める ── sorry-first workflow

2026年、ムンクレスの『位相空間論』という教科書 を Isabelleで形式化 した研究があります。

そこで採られた手順が、過去に公開済みの記事で紹介した「sorry-first workflow」です。

1. 証明の骨組みを書き、そのすべての行に sorry と書く
2. （中略）
3. sledgehammer が失敗したら、その行をより細かい have のブロックへ分解し、繰り返す

言語そのものを変えるのではなく、書き方の側を定めるという方向です。

出典:"Munkres' General Topology Autoformalized in Isabelle/HOL", arXiv:2604.07455, 2026年

方向その３:変換する ── Apply2Isar

2026年 に、Apply2Isar が発表されました。

これは、タクティクスタイル で書かれた証明を、自動的に Isar に変換するものです。

論文には、両スタイルの記法の違いが明記されています。

In Isabelle/HOL, declarative proofs written in the Isar language are widely appreciated for their readability and robustness.

However, some users may prefer writing procedural "apply-style" proof scripts since they enable rapid exploration of the search space.

（筆者による日本語訳）

Isabelle/HOL において、Isar 言語で書かれた宣言的な証明は、その読みやすさと頑健さから広く評価されている。

しかし、探索の空間を素早く調べられるという理由で、手続き的な「apply スタイル」の証明スクリプトを書くほうを好む利用者もいる。

出典
"Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar", 2026年

探索の段階ではタクティク、保守の段階では宣言的スタイル。

証明を書いている間は、タクティクの速さを使い、書き終えたものを記録するときは Isar の形で残す。

その両方の利点を得るための発想 です。

方向その４:　移植する ── Lisar

同じ2026年に、Isabelle の Isar を Lean 4 に持ち込むライブラリも公開されました。

このライブラリを生み出したのは、AIでした。

過去に公開済みの記事で詳しく扱っていますので、ここでは繰り返しません。

出典
nomeata/lean-lisar

ProofAug ── 構造を利用する

第７部で見た ProofAug が、５つ目の方向です。

この研究は、宣言的スタイルを変えようとしません。
むしろ、その構造を積極的に利用します。

論文の説明を見てください。

based on the observation that regardless of correctness, full proofs contain rich structural information from which valid semi-proofs of varying granularities can be derived.

（筆者による日本語訳）

正しいかどうかに関わらず、完全な証明は豊かな構造の情報を含んでおり、そこから様々な粒度の妥当な semi-proof（部分的な証明）を導き出せる、という観察に基づいている。

出典
"ProofAug", ICML 2025

少しわかりづらい文ですので、補足説明します。

「完全な証明」 とは、モデルが最初に書き上げた証明のことです。
細部まで書かれていますが、そのどこかに誤りがあり、処理系の検査を通りません。

「semi-proof」 とは、この記事の冒頭で取り上げました。

sorry を置いて、一部を未証明のまま残した証明を指します。
この語に定訳はなく、ProofAug の論文が用いた造語です。

「妥当な」 とは、その状態で処理系の検査を通るという意味です。

sorry を置いた箇所は未証明のままですが、それ以外の部分に誤りがないことを、処理系が確かめることができます。

「様々な粒度の」 とは、sorry をどこに置くかによって、何通りもの形が作れるということです。

細かく刻んで多数の sorry を置くこともできれば、大きくまとめて少数の sorry で済ませることもできます。

つまり、こういうことです。

誤りを含む証明であっても、書かれた構造そのものは使えます。

どこまでが正しく、どこから先が誤っているのか。

それを見極めて、誤っている部分だけを sorry に置き換えれば、検査を通る形が得られます。

そして、その置き換え方を変えることで、粒度の異なる複数の骨格が手に入ります。

手順は、次のとおりです。

1. まず、モデルに証明を丸ごと書かせる（骨格を書かせるのではない）
    
2. その証明から、処理系の検査を通る最大の semi-proof を見つける
    
3. 自動証明の仕組みが隙間を埋められなければ、より粗い semi-proof へ後退する
    
4. 以上を繰り返す

「粒度」 という言葉の意味は以下のとおりです。

細かい粒度 ── 証明の細部まで書かれた状態
粗い粒度 ── 骨組みだけが残った状態

そして、粒度を変えられるのは、証明に構造があるからにほかなりません。

過去に公開済みの記事で見た have による分解を、思い出してください。 うまくいかない行を、より細かい have に分けました。

ProofAug は、その逆をします。

うまくいかなければ、より粗くする。

そして自動証明の仕組みに、より大きな隙間を任せます。

ProofAug の入力・出力

• 入力 ── 定理の主張と、モデルが生成した証明の候補。

• 出力 ── 粒度を変えた semi-proof の列。

• 特徴 ── 専用の学習を行っていません。

既存のモデルが生成した証明を、後から加工する仕組みです。

Kimina-Prover の1.5Bのモデルの成績を、44.3%から50.4%へ引き上げることに成功しました。

４つの方向を、整理します

方向	何をするか	代表的な研究
言語を作り変える	構文を減らした新しい言語を設計する	MiniLang（2025年）
書き方を定める	sorry を使う手順を確立する	sorry-first workflow（2026年）
変換する	タクティクスタイルから宣言的スタイルへ自動変換する	Apply2Isar（2026年）
移植する	別の言語へ持ち込む	Lisar（2026年）
構造を利用する	粒度を変えながら探索する	ProofAug（2025年）

冗長性に対する評価が、正反対に分かれています 。

• MiniLang は「構文の冗長性」を問題と呼びます。

• ProofAug は「豊かな構造の情報」と呼びます。

同じものを見て、正反対の評価結果が出ています。

そして、どちらも成果を出しています。

この対立には、まだ決着がついていないのです。

補足: 機械が立てた予想を、機械が証明した

第８部の主題からは外れますが、ご紹介したい事実があります。

はじめにの対話で、1980年代の GRAFFITI という自動予想生成システムに触れました。

2026年の AlphaProof Nexus が、グラフ理論のある予想 を 証明 しました。

その予想を立てたのは、1996年の GRAFFITI だったのです。

論文には、こう書かれています。

The problem was posed by Graffiti, an automated conjecturing system, in 1996, and points to an interesting future opportunity to close the loop between AI-based conjecturing and proof.

（筆者による日本語訳）

この問題は、自動予想生成システムである Graffiti によって1996年に提起されたものであり、AIによる予想とその証明のあいだで輪を閉じるという、興味深い将来の可能性を指し示している。

出典:"Advancing Mathematics Research with AI-Driven Formal Proof Search", arXiv:2605.22763, 2026年

予想を立てる仕組みと、証明する仕組みが、30年を隔ててつながりました。

ただし、論文では、「将来の可能性」 と綴られています。

輪は、まだ閉じていません。

本連載の記事

• 第1回:AIが数学の証明を書けるようになった6年間（この記事）
   
• 第2回:タクティク記法と宣言的スタイル記法、AIはどちらで学ぶのか
   
• 第3回:どの国が、この分野を牽引しているのか
   
• 第4回:形式化コードと自然言語、どちらを求めているのか

次回予告

連載の第２回の記事 では、AIの内部構造 を扱います。

定理証明を行うAI は、タクティク記法 と 宣言的スタイルの記法のどちらのスタイルで書かれた学習データを学ぶのか？

そして、そのAIから生成される定理証明コードは、どちらのスタイルで綴られているのか？

これまでに提案されたAIが、実際に学習した学習用データと、それぞれのAIから生成される証明コードを具体的に眺めることで、見定めていきます。

10個 の Neural Theorem Prover について、入力・出力・学習データ を調べてみたいと思います。

関連記事

実務での形式検証

• 「テスト通ったから大丈夫」を卒業しよう──LLM生成コードをLean4/Dafnyで形式検証する方法
   
• 96%の開発者がAI生成コードを信用していないのに48%が検証せずデプロイしている──Leanstralという解決策

定理証明支援系の入門

• 依存型を使わないIsabelle/HOL とは何か ── AWS のクラウド基盤を検証した定理証明系は、なぜ証明を自動で探せるのか
   
• Lean 4 とは何か
   
• Rocq（旧名 Coq）とは何か

形式手法と、その限界

• 形式証明は「仕様が人間の意図を反映しているか」は保証しない
   
• AI Agent は社会規範に反していても、論理的に正しければ実行可能と判断してしまう

出典

分野の全体像

• "A Survey on Deep Learning for Theorem Proving", arXiv:2404.09939
• "From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier", arXiv:2607.07779, 2026年
• "TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics", arXiv:2606.09450, 2026年

ベンチマーク

• "miniF2F: a cross-system benchmark for formal Olympiad-level mathematics", ICLR 2022
• openai/miniF2F（公式リポジトリの統計）
• "PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition", arXiv:2407.11214

時系列で扱った主要な研究

• Stanislas Polu, Ilya Sutskever, "Generative Language Modeling for Automated Theorem Proving", arXiv:2009.03393, 2020年（GPT-f）
• Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, Yuhuai Wu, "LISA: Language Models of ISAbelle Proofs", AITP 2021, 378〜392頁
• Albert Qiaochu Jiang ほか, "Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers", NeurIPS 2022, 8360〜8373頁
• Guillaume Lample ほか, "HyperTree Proof Search for Neural Theorem Proving", NeurIPS 2022, 26337〜26349頁
• Albert Q. Jiang ほか, "Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs", ICLR 2023
• Emily First, Markus N. Rabe, Talia Ringer, Yuriy Brun, "Baldur: Whole-Proof Generation and Repair with Large Language Models", ESEC/FSE 2023
• Kefan Dong, Tengyu Ma, "STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving", arXiv:2502.00212, 2025年
• "Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving", arXiv:2507.23726, 2025年
• "DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning", arXiv:2504.21801, 2025年
• Numina & Kimi Team, "Kimina-Prover Preview", arXiv:2504.11354, 2025年
• Yong Lin ほか, "Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving", arXiv:2502.07640, 2025年

AlphaProof と IMO 2024

• AI achieves silver-medal standard solving International Mathematical Olympiad problems, Google DeepMind, 2024年
• Thomas Hubert ほか（Google DeepMind）, "Olympiad-level formal mathematical reasoning with reinforcement learning", Nature, 2025年11月12日
• IMO 2024 P6, Google DeepMind
• AlphaProof's Greatest Hits, Rishi Mehta, 2024年11月17日
• Prithwish Jana ほか（ジョージア工科大学）, "ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings", arXiv:2510.15681

Lean と Isabelle の差

• "HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement", arXiv:2505.15740, 2025年
• Haoxiong Liu, Jiacheng Sun, Zhenguo Li, Andrew C. Yao, "ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis", ICML 2025, 39568〜39586頁

宣言的スタイルに関する研究

• "A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL", 2025年（MiniLang）
• "Munkres' General Topology Autoformalized in Isabelle/HOL", arXiv:2604.07455, 2026年
• "Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar", 2026年
• nomeata/lean-lisar, 2026年

予想の生成

• "Computer assisted discovery: Zero forcing vs vertex cover", arXiv:2209.04552（GRAFFITI）
• "In Reverie Together: Ten Years of Mathematical Discovery with a Machine Collaborator", arXiv:2507.17780
• "Discovering New Theorems via LLMs with In-Context Proof Learning in Lean", arXiv:2509.14274

AIによる数学の成果

• George Tsoukalas, Anton Kovsharov, Sergey Shirobokov ほか（Google DeepMind）, "Advancing Mathematics Research with AI-Driven Formal Proof Search", arXiv:2605.22763, 2026年5月21日（AlphaProof Nexus）
• Boris Alexeev, Moe Putterman, Mehtaab Sawhney, Mark Sellke, Gregory Valiant, "Short proofs in combinatorics and number theory", arXiv:2603.29961, 2026年
• Alberto Romero, The Month AI Conquered Math: The Full Story, The Algorithmic Bridge, 2026年8月
• Terence Tao on AI in mathematics (and beyond)