出典：SiliconAngle
数学の世界には、長らく奇妙な二層構造が存在している。「証明された定理」と「誰もが反論できない形で検証された定理」は、同じではない。人間の数学者が書いた証明は、突き詰めれば「その分野の専門家たちが読んで、論理的に正しいと合意した」という話だ。どれだけ精緻に書かれていても、人間の目を通す以上、見落としや解釈の揺れが忍び込む可能性はゼロにならない。
フェルマーの最終定理は、その問題を象徴する存在だった。1637年にフェルマーが余白に書き残した命題は、358年間誰も証明できなかった。1995年、アンドリュー・ワイルズがついに証明を完成させたとき、数学界は沸いた。だがその証明は129ページに及ぶ超高難度の論文で、内容を完全に追える数学者が世界に何人いるかというレベルの代物だった。「証明されたことになっている」という状態は、それ以来30年近く続いてきた。
コンピュータに一行ずつ検証させるには、別の言語に翻訳し直す必要がある。それが「形式証明」と呼ばれる手法で、Leanというプログラミング言語で記述されたコードとして証明全体を再構築する作業だ。人間の直感や暗黙の了解を一切排除し、機械が判定できる論理の連鎖に書き直す。この翻訳作業は途方もなく難しく、専門家たちはフェルマーの定理への適用には数年かかるだろうと見ていた。
Anthropicは、それを11日で終わらせた。Claudeを使って。
この話が面白いのは、AIが新しい定理を発見したわけではない点だ。やったのは既存の証明の「翻訳」だ。しかしその翻訳の規模と速度は、数学とAIの関係を根本から問い直すような水準に達している。
完成したLeanコードは1300万行。これはこれまで作られた形式証明の中で最大規模のファイルだ。生成された出力トークンは600億、途中で証明した中間定理の数は2万9500以上。数十のエージェントが並列で作業を進め、最初の試みは失敗し、オープンソースツールへのアクセスを与えることで突破口が開いた。
こうした取り組みが持つ意味は、速度だけではない。形式証明が完成したということは、フェルマーの最終定理の正しさを、今後は人間の合意ではなくコンピュータの検証に委ねられるということだ。数学的真実の「担保のしかた」が変わる。
Anthropicがこの結果を公開したのは、ちょうど1ヶ月前にClaudeによるリーマンΖ関数に関する新たな知見の発表があった直後だ。単発の成果ではなく、AIによる数学研究の地続きの進展として読む必要がある。
3行まとめ
- AnthropicがClaudeを活用し、フェルマーの最終定理の証明をコンピュータが検証可能な形式証明（Leanコード）に変換することに成功した
- 専門家が数年かかると予測していた作業を11日間で完了し、1300万行のコードと2万9500以上の中間定理を生成した
- Anthropicは今回の詳細を自社ブログで公開しており、約1ヶ月前にもClaudeによるリーマンΖ関数の新知見発見を発表している
※以下は詳細
フェルマーの最終定理とは何か
フェルマーの最終定理は、正の整数の性質に関する命題で、1637年にフランスの数学者ピエール・ド・フェルマーが提唱した。n が3以上の整数のとき、xⁿ + yⁿ = zⁿ を満たす正の整数の組は存在しない、という内容だ。提唱から358年間にわたって誰も証明できなかったが、1995年にイギリスの数学者アンドリュー・ワイルズが129ページの論文で証明を完成させ、数学界最大の懸案のひとつに決着がついた。
形式証明とは何か、なぜ難しいのか
数学者が書いた通常の証明は、専門家が論理を追うことで正しさを確認する。これに対して「形式証明」は、Leanと呼ばれるプログラミング言語を使い、証明の全ステップをコンピュータが機械的に検証できるコードとして書き直したものだ。人間の解釈や暗黙の前提が入り込まない分、検証の確実性が大幅に高まる。
ワイルズの証明をこの形式に変換する作業は、数学的な難易度と作業量の両面で極めてハードルが高く、専門家の間では完了まで数年かかるという見方が一般的だった。
11日間・1300万行・2万9500の中間定理
Anthropicの研究チームは社内の研究用モデルを活用し、11日間でこの変換作業を完了した。完成したLeanコードは1300万行に達し、これまでに作られた形式証明ファイルの中で最大規模となった。
作業の過程で、モデルは数十のエージェントを並列起動し、合計600億トークンの出力を生成した。また、最終的な証明に至る過程で2万9500以上の中間定理を個別に証明している。当初の試みは失敗に終わったが、Prove2Meというオープンソースツールへのアクセスを与えたことで作業が前進し、完成にこぎつけた。
数学者からの反応と公開の経緯
Anthropicは今回のプロジェクトの詳細を自社ブログで公開した。数学者のKevin Buzzardは「AIによる自動形式化の成果物が、他の研究の上に積み重ねられるほど堅牢になった」とコメントしている。
全体まとめ
AnthropicはClaudeを使い、フェルマーの最終定理の証明をコンピュータが検証可能な形式証明へ変換することに成功した。専門家が数年かかると見ていた作業を11日間で完了し、1300万行のLeanコードと2万9500以上の中間定理を生成した。作業には数十の並列エージェントと600億トークンの出力が費やされ、オープンソースツールのProve2Meの活用が突破口となった。完成したファイルはこれまでで最大規模の形式証明となっている。Anthropicはこの約1ヶ月前にもClaudeによるリーマンΖ関数に関する新たな知見の発見を発表しており、AIを活用した数学研究の成果の公開が続いている。