Anthropic、Claude がフェルマーの最終定理を Lean で完全形式化——11日間で1300万行、機械検証を通した証明を公開

Anthropic が9月4日、同社の Claude がフェルマーの最終定理の証明を定理証明支援系「Lean」の上で最後まで形式化し、機械による検証を通したと発表しました。
形式化というのは、人間の言葉で書かれた数学の証明を、計算機が一行ずつ正しさを確かめられる形へ書き直す作業のことです。
できあがったのは約1300万行の Lean コードで、途中で使う補題まで含めて3万300個の定理が証明され、うち2万9500個が最終的な証明に使われています。
Claude はこれを11日間、ほぼ自律的に書き進めたとされています。

鍵になったのは、コロンビア大学の Tianyi Peng 氏らが公開している「Prove2Me」という共同作業用のオープンな基盤でした。
証明すべき命題を有向グラフとして並べ、多数のエージェントが別々の枝を同時に埋めていける仕組みで、Anthropic は最初の試みがうまくいかなかったあとにこれを組み合わせています。
形式化の対象は1995年のワイルズの証明そのものではなく、その後に整理された簡略版です。
Lean の標準的な三つの公理だけを前提に組み立てられ、正しさは Lean のコンパイラが確認しています。

形式化の研究で知られる数学者のケヴィン・バザード氏は、専門家が見込んでいたよりはるかに短い時間で到達したと評しています。
同氏自身、長いあいだ同じ定理の形式化に取り組んできた立場です。
現代数学の論文を機械が読める形へ移していく道が、思っていたより早く開きつつあるということなのだと思う。

サイトやシステムの運用からは遠い話に見えますが、注目したいのは「AIが出したものを、人間の目視ではなく機械で検証しきった」という点です。
生成AIの出力は、もっともらしく見えるかどうかでしか判定できない場面がまだ多い。
検証の仕組みを外側に用意できる領域から、AIの使いどころが着実に広がっている——今回の発表は、その一例として読むのがよさそうです。