AIに「証明する価値のある数学」を発見させる

2026年9月25日読了目安 3 分

導入

大規模言語モデルは、難しい数学問題を解くだけでなく、形式化された証明を生成する能力も高めている。すると次の課題が現れる。モデルが大量の命題を提出し、正しい証明まで作れるようになったとき、その中から本当に研究する価値のあるものをどう選ぶのか、という問題である。

論文「Learning to Discover Interesting Mathematics」は、証明の成功率だけを最適化するのではなく、数学的発見の候補を順位付けするための実用的な指標を設計した。狙いは、正しいだけでなく、既存の知識の単純な再現ではない命題を見つけることにある。

面白さを長さの比率で表す。 研究では、定理の内在的な面白さを、証明の長さを命題の長さで割った値として定義する。短い主張に対して長く構造的な証明が必要なら、単純な帰結よりも豊かな内容を含む可能性がある、という直観に基づく。
前提付きの証明難易度を予測する。 候補を評価するには、与えられた前提と数学ライブラリを使った場合に、証明がどれほど難しいかを見積もる必要がある。チームはこの目的のために27B規模のモデルを学習し、最先端の汎用モデルより高精度に予測できたと報告している。
生成と検証を循環させる。 システムは候補定理を生成し、指標に基づいて選別し、証明を検証する。検証済みの結果は拡張され続ける形式数学ライブラリに追加され、次の探索で利用される。

論文によれば、指標を最適化することで、生成された定理の面白さは4.3倍になった。また、Mathlibと大幅または完全に重複する結果の割合は91.9%から30.6%に下がった。これは、既存ライブラリの言い換えや近い再構成だけでなく、より分布外にある形式数学を生成できる可能性を示している。

この研究の重要性は、「面白い」という曖昧な判断を、学習や探索に利用できる信号へ変換した点にある。もし他の数学分野でも下流の有用性との相関が確認されれば、限られた計算資源を、将来の研究につながりやすい予想へ重点的に配分できるかもしれない。

ただし、証明が長いことは数学的に重要であることを意味しない。形式化の効率が悪いだけで長い証明になる場合もあり、短い証明が深い結果を示すこともある。そのため、この指標は最終評価ではなく候補選別の補助信号として理解するのが適切だ。概念的な意義や一般性、実際の有用性を判断する役割は、なお数学者に残る。

それでも、命題の生成、機械検証、候補の順位付け、ライブラリの拡張を繰り返す仕組みは、自己拡張型の形式数学ライブラリへの道筋を示している。今後の課題は、単に難しい証明を増やすのではなく、人間が理解し、さらに研究したいと思える数学を生み出せるかどうかだ。