フェルマーの最終定理、機械が最後まで検証できる形になった——11日・1,300万行、Anthropicが公開

Anthropicが2026年9月4日、フェルマーの最終定理の証明を、計算機が最後まで検証できる形に書き下したと発表しました。証明支援系Leanで書かれ、規模は1,300万行に達します。

何が新しいのか

証明そのものが新しいわけではありません。フェルマーの最終定理は1995年にAndrew Wilesが証明し、その後Henri Darmon・Fred Diamond・Richard Taylorがより簡潔な形にまとめています。数学の中身は変わっていません。

新しいのは、その証明を機械が一行ずつ確かめられる形に移したことです。人間が読んで納得する証明と、計算機が公理から順に検証できる証明は別物で、後者に書き直す作業を形式化と呼びます。今回はLeanの標準的な3つの公理だけから導かれるところまで到達したとしています。

数字は次のとおりです。

どう作ったか

中心になったのは、Anthropicの研究者Tianyi Peng氏らがColumbia大学の共同研究者と設計したProve2Meという、形式化を分担するための場です。証明したい命題を細かく割り、依存関係を有向非巡回グラフ（DAG）として持ち、複数の作業単位が並行して埋めていく形をとっています。命題の書き方が揃っているかを確かめるcomparatorも置かれています。

土台にはコミュニティが積み上げてきた証明ライブラリMathlibがあり、形式化そのものはImperial College LondonのKevin Buzzard氏が主導するFLTプロジェクトが進めてきたものです。今回の成果は、その蓄積の上に乗っています。

うまくいかなかったところも書かれている

発表は成功だけを並べてはいません。

• 初期には作業の状態を見失って分担が成り立たなくなる段階があった
• 失敗に終わった初期の試みが、最終的に使われなかった行のおよそ7%を占めた
• 出来上がった証明は必要以上に長い可能性がある（Mathlibと比べると効率が悪い）
• Prove2Meが無ければ成功していなかったとしている

⚠️ トークンを大量に使う進め方であることも明記されています。約60億出力トークンという数字は、同じやり方を他の定理へそのまま広げるときの費用を考える材料になります。

速さの実験

同じ枠組みで、Hardy-Littlewoodの円周法を使ったVinogradovの三素数定理の形式化を3日で終えたことも報告されています。フェルマーの11日と並べると、規模の小さい対象では日単位で片が付くことを示す例になっています。

どう受け止めるか

形式化は、数学の正しさを人の査読だけに委ねない道を開くものです。長大な証明ほど人手での検証は難しく、フェルマーの最終定理はその代表でした。機械が確かめられる形になったこと自体が、今回のいちばんの成果です。

一方で、これは「AIが定理を発見した」という話ではありません。既にある証明を、確かめられる形に移した仕事です。数学の新しい結果が出たわけではない点は、読み違えないほうがよいところです。