Anthropicは2026年9月4日、Claudeが約11日でフェルマーの最終定理の既存の証明をLeanへ形式化し、機械検証を完了した研究成果を公開しました。9月5日にも報道されましたが、実行自体は8月に終了しています。今回のニュースは成果公開であり、未解決問題をその日に解いたという話ではありません。
新たな発見ではなく、一歩ずつ検証する
フェルマーの最終定理は、2より大きい整数nについて、aⁿ+bⁿ=cⁿを満たす正の整数a、b、cは存在しないという命題です。Andrew Wilesの証明は1995年に発表済みです。今回の研究は既存の数学的な道筋をLeanで扱える形式言語に移しました。
数学の論文では専門家に自明な手順を省けますが、機械検証には定義と推論を明示する必要があります。公開リポジトリにはビルド検査と命題の比較手順があり、単に実行が終わるだけでなく、公理と結論がMathlibの対象の定理に対応することを確認します。
複数のAIはどう協力したのか
Anthropicによると、数十のAgentが約1,300万行のLeanコードを作成しました。Prove2Meは定理間の依存関係を整理し、再利用できる結果を検索できるようにします。会話を延ばし続けるのではなく、大規模な共同作業の状態を共有する仕組みです。
Imperial College Londonの数学者Kevin Buzzardも、自らコードをコンパイルし比較ツールを実行して成功したと報告しています。一方、巨大な形式化成果物と、読みやすく保守・再利用しやすい数学ライブラリは別物だと指摘しており、人間による理解は依然必要です。
Claudeの契約だけで再現できる機能ではない
実行にはClaude Fable 5.1とおおむね同等の内部研究モデルと複数Agent用の実行環境を使い、研究者も時折大まかな指示を出しました。公表されたのは約60億出力tokensで、実際の請求額ではありません。一般アカウントの無料機能や、公開API単価から確定できる研究費として紹介するのは不適切です。
コードは公開されていますが、リポジトリは保守を行わず貢献も受け付けない研究成果物と明記しています。検討・検証用の資料であり、長期サポート付きAPIでも、任意の問題をチャットに貼れば正答が保証される機能でもありません。
重要なのは答えを検証できること
一般のAI利用者にとっての教訓は、答えの生成と検証を分けることです。流暢な説明は正しさの証拠ではありません。今回は明示された命題、公開コード、形式検証ツールがあるため結果を調べられます。大規模検証へのAIの貢献を示す一方、あらゆる専門分野に同じ検査条件が整ったわけではありません。
