フェルマーの最終定理をClaudeが11日と1300万行で機械証明した

3万の定理を形式化し1300万行　Claudeが11日で完成させた

Anthropicが2026年9月4日にClaudeによるフェルマーの最終定理の形式化を発表しました。形式化とは数学の証明をコンピューターが検証できる形に書き直す作業です。人間向けの論文では「明らか」として省略される手順もすべて厳密に記述します。

フェルマーの最終定理は350年以上にわたって未解決でしたが1995年にアンドリュー・ワイルズが129ページの論文で証明しました。正しさの確認だけでも数カ月かかっています。インペリアル・カレッジ・ロンドンのケビン・バザード氏は2024年からLeanでの形式化プロジェクトを率いています。初期の作業計画だけで86ページに達しており完了まで数年かかる見込みでした。

Anthropicの研究者ティエンイー・ペン氏がClaudeに作業させたところ11日間で完了しました。約3万300件の定理を形式化し最終的に約2万9500件を使っています。生成したLeanコードは約1300万行でLean向け数学ライブラリMathlibの5倍以上です。Anthropicはこれを初の完全な機械検証済み証明だとしています。

進捗を見失ったAI　Prove2Meで管理して解決した

数十のClaudeエージェントが概念の定義や中間定理の証明を分担しました。ただし初期の試行ではエージェントがプロジェクト全体の進捗を把握できなくなり、互いの成果を再利用できない状態に陥っています。

解決に使われたのがペン氏らが開発した数学形式化プラットフォームProve2Meです。定理の依存関係をDAG（有向非巡回グラフ）で管理し各エージェントが次に取り組むべき定理を確認できるようにしました。定理の記述と証明を別ファイルに分けてコンパイルを速くし、自然言語の説明を付けて既存の証明を検索・再利用しやすくしています。

AIの長期自律作業　進捗管理の仕組みが結果を分けた

今回の結果はAIの能力だけでは長期の自律作業がうまくいかないことを示しています。11日間にわたる作業では「何がどこまで終わったか」「次に何をすべきか」を管理する仕組みが成否を左右しました。AIを複数動かすだけでは作業が進まなかった初期の失敗がそれを裏付けています。

AIにまとまった仕事を任せるときはタスクの分解と進捗の可視化が欠かせません。コードの生成能力だけでなくプロジェクト管理の設計まで含めて考える必要があります。Anthropicは今後人間向けの論文とあわせて形式化済みの証明を作るのが一般的になると予想しています。

証明はGitHubで全文公開　Lean 4で検証もできる

完成した証明はLeanによるチェックを通過しGitHubで公開されています。Leanの標準的な3つの公理だけに依存しており未証明部分を一時的に通す「sorry」も含まれていません。Mathlibに収録されているフェルマーの最終定理の記述と証明対象が一致することも確認済みです。

さらにRustで書かれた独立したLeanカーネルnanodaでも100万件以上の宣言をエラーなしで検査できたと報告されています。Lean 4の環境がある人は自分の手元で証明をビルドして正しさを確認できます。