2026年9月4日、Anthropicはフェルマーの最終定理（FLT）について、初めて完全にコンピュータで検証された証明を公開した。ClaudeがLeanという証明支援言語で証明を書き、11日間ほぼ自律的に作業したという。ワイルズの証明は129ページあり、確認に何カ月もかかった。人間がLeanに書き直すと何年もかかると見られていた作業を、AIが最初から最後まで通した例になる。今回の新しさは、新しい数学を作ったことではない。証明を機械で検証したことにある。
発表内容
このプロジェクトは、AnthropicのTianyi Peng氏が始めた。同氏のコロンビア大学のグループは、AIで数学を形式化するツールを作っている。ClaudeがFLTの形式化を進められるかを試したところ、証明が最後まで完成した。
- 作業期間：11日間、ほぼ自律的に作業
- Leanのコード：1300万行。コミュニティの主要な数学ライブラリMathlibの5倍以上
- 途中で証明した定理：30,300個。そのうち29,500個を最終的な証明で使った
- 数十体のClaudeエージェントが分担し、概念の定義、中間定理の証明、より難しい命題の証明を重ねていった
- 証明の土台は、Darmon、Diamond、Taylorによるワイルズの証明の簡略版
- 人間の数学的な関与は、Peng氏がときどき出す大まかな指示だけ。例：「Jacobian as a scheme sounds high priority」
完成した証明を受け取ったKevin Buzzard氏（インペリアル・カレッジ・ロンドン）は、次のようにコメントしている。同氏は2024年から、Leanでフェルマーの最終定理を形式化する複数年のコミュニティプロジェクトを率いてきた。
This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics. (…) we learn that AI autoformalization artefacts are now robust enough to be built upon; the proof is multi-layered.
成功の鍵は、作業基盤をProve2Meに切り替えたことだった。Prove2MeはPeng氏らが設計した、数学の形式化のためのオープンな共同作業プラットフォームだ。最初の試みでは、エージェントがプロジェクトの状態を見失い、協力がうまくいかなかった。元記事によると、失敗した試みの成果は最終的な証明の定型部分を除いた行の約7%に使われている。Prove2Meは主に次の3点で役立った。
- 定理の依存関係をDAG（有向非巡回グラフ）で管理した。エージェントは次にどの証明に取り組むかをここで決めた。記憶の劣化を抑え、複数のエージェントが並行して作業できた
- 定理の主張と証明を別々のファイルに分け、両者のつながりは別に管理した。これでLeanのコンパイルが速くなり、使うリソースも減った
- 各定理に自然言語の説明を付けた。検索と再利用がしやすくなり、証明の道筋も単純になった
なぜ重要か
元記事によると、新しい証明が正しいと確信できるまで理解するには、数カ月から数年かかることがある。ワイルズも1993年に証明を発表したが、検証の途中で決定的な穴が見つかった。修正に約1年かかり、正しい証明が出版されたのは1995年5月だった。
As AI produces ever more proofs, the ability to easily formalize work can lighten the burden of evaluating new results (a process that can take years).
AIが作る証明が増えるほど、それを人間がレビューする負担も重くなる。Anthropicは形式化をその負担を軽くする手段と位置づけ、数学の知識体系を信頼しやすくなるという期待を示している。
現時点での未確定事項
- 使ったClaudeのモデル名とバージョン：取得できた原文には明記されていない
- 計算コストと使ったリソースの量：元記事では具体的な数値は示されていない
- 外部による再検証：Claudeの思考ログには「modulo re-check」という表現がある。第三者がどこまで独立に再確認したかは、原文の範囲では分からない
- Buzzard氏のコミュニティプロジェクトとの関係：成果をどう取り込むか、並行して続けるのかは書かれていない
- 取得できた原文の範囲：取得したテキストはマルチエージェント構成の説明の途中で終わっている。後半の詳細は確認できていない
まとめ
- Claudeは11日間ほぼ自律的に作業し、Lean 1300万行でFLTの証明を最初から最後まで機械検証可能な形にした
- 成功の鍵は、DAGで進捗を管理するProve2Meと、Claude Codeベースのマルチエージェント構成だった
- 今回の新しさは数学的な発見ではなく検証にある。モデル名、コスト、外部の再検証はまだ明らかになっていない
実装家の視点で一番注目したいのは、「最初はエージェントが状態を見失って失敗した」という点だ。依存関係をDAGで外に出して管理したら、うまく回り始めた。数十体のエージェントで長時間の仕事を回すときの問題は、モデルの賢さより、状態をどこに持つかにある。これは数学に限らず、Claude Codeで大きな実装を並列に回すときの設計にもそのまま使える教訓だと思う。
コメント