9月4日、SiliconAngleが「Anthropic uses Claude to formalize proof of Fermat's Last Theorem」と題した記事を公開した。AnthropicがClaudeを用いてフェルマーの最終定理の証明をコンピュータで自動検証可能な形式に変換することに成功したという内容だ。数学コミュニティが「数年かかる」と見込んでいた作業を11日で完了させたとされる。

「数年かかる」と見込まれた作業を11日で完了

フェルマーの最終定理は1637年に提唱された数論上の命題で、数百年間にわたり未解決のままだった。1995年に数学者Andrew Wilesが129ページに及ぶ証明を発表し、解決に至った。その証明の検証だけでも数カ月を要したとされる。

Anthropicが今回取り組んだのは、このWilesの証明の形式化（formalization）だ。形式化とは、自然言語や記号で書かれた数学の証明を、コンピュータが自動的に検証できるコードに変換する作業を指す。使われるのはLeanという定理証明支援言語で、数学者が仮説を機械的に検証するために設計された専用構文だ。形式化された証明はLeanコードの形を取り、人間によるミスを排除できるほか、数学者間での知識共有も容易になる。

数学コミュニティではWilesの証明の形式化に数年かかると予想されていた。Anthropicはこれを社内研究モデルを用いて11日で完成させた。同モデルは同社が社内研究モデルと表現したモデルであり、Claude Fable 5.1相当とされている。

生成されたLeanコードは1300万行にのぼり、同種のファイルとして史上最大規模だ。処理中にはモデルが数十のエージェントを立ち上げ、60億トークンの出力を生成。途中で証明した中間定理（intermediate theorems）の数は2万9500件以上に達した。

ブレークスルーのカギはオープンソースツール「Prove2Me」

Anthropicの最初の試みは失敗に終わっている。突破口となったのは、Prove2MeというオープンソースツールへのアクセスをClaudeに与えたことだった。Prove2Meは長い処理ワークフローの中でAIエージェントが最適な次のステップを判断しやすくするソフトウェアで、推論コストの削減にも効果があるという。

形式化が難しい理由の一つは、数学の証明が本来非常に簡潔に書かれている点だ。コンピュータが理解するために必要な説明が省略されており、開発者が手動で補う必要がある。また、証明内の論証が互いに積み上げられる構造を持つため、Leanコードの1行のミスがその後の全コードを無効にしてしまうリスクもある。

今回ClaudeがLeanコードの生成に用いた研究成果の持ち主である数学者Kevin Buzzardは次のようにコメントしている。

「代数、調和解析、幾何学、数論にわたる自動形式化が実現しており、AIによる形式化の成果物が、その上にさらなる構築ができるほど堅牢になっていることがわかる。この証明は多層構造だ」

伏線：1カ月前のリーマン予想関連の報告

今回の発表に先立ち、Anthropicはこの約1カ月前にも関連する成果を公表していた。Claudeを使ってリーマンゼータ関数（リーマン予想の核心にある数学的対象）に関する新たな知見を得たことを報告している。今回のフェルマー形式化は、その流れを受けたより大規模な取り組みと位置づけられる。

競合OpenAIも数学研究でLLMを活用

同様の動きは競合他社でも見られる。OpenAIは先月、最新モデルの「Astra」を用いて複数のErdős問題を解き、理論計算機科学における未解決問題をいくつか前進させたと発表した。LLMを数学研究に本格投入する競争が、主要AI企業間で加速している。

詳細はAnthropic uses Claude to formalize proof of Fermat's Last Theoremを参照していただきたい。