Claudeがフェルマーの最終定理を11日で形式化、新証明ではない

Anthropicは2026年9月4日、Claudeを使った複数エージェントがフェルマーの最終定理を11日間でLean形式化したと発表した。Anthropicの研究発表 によると、Claudeは約1,300万行のLeanコードを生成し、3万300件の定理を証明、そのうち約2万9,500件を最終成果で使用した。作業には数十のエージェントと共同形式化基盤Prove2Meが使われ、出力トークンは約60億に達した。

ただし、これはClaudeが未知の解法を見つけた、あるいはアンドリュー・ワイルズらとは異なる新証明を発見したというニュースではない。9月5日付の AI Stack Currentの検証記事 も、成果を既知の証明経路に基づく完全な形式化と位置付けている。新しいのは数学的結論ではなく、極めて大きな既知の論証を短期間で機械検査可能な成果物へ変換した工程と規模だ。

11日間で完成したもの

完成したのは、人間向けの証明を要約した文章ではなく、フェルマーの最終定理へ至る定義、補題、推論と依存関係をLean 4で記述した形式証明である。最終命題は、3以上の自然数nと正の自然数a、b、cについて、aのn乗とbのn乗の和はcのn乗にならない、という通常の自然数版を表す。

人間向けの論文では既知または自明として省略できる段階でも、Leanでは型、前提、定義、参照する補題を明示しなければならない。Claudeのエージェント群は概念の定義、中間定理の証明、完成済み成果の検索と再利用を分担し、最終命題まで論理的につながるコードを組み立てた。

この共同作業を支えたのがProve2Meだ。定理同士を有向非巡回グラフとして管理し、未解決の命題と利用可能な成果をエージェント間で共有したほか、定理の宣言と証明を別ファイルに分けてコンパイル負荷を抑えた。初期の試行ではエージェントがプロジェクト全体の状態を追えず連携が崩れたため、今回の結果はClaude単体の一度きりの回答ではなく、モデル、複数エージェントの制御、共有基盤、Leanの検査を組み合わせたシステムの成果と見る必要がある。

発見、証明、形式化、機械検証の違い

発見は、未知の命題や数学的関係、解法を見いだすことを指す。フェルマーの最終定理そのものは以前から知られ、ワイルズとリチャード・テイラーの仕事によって1990年代に証明が完成しているため、今回の成果を定理の発見とは呼べない。

数学的証明は、命題が正しい理由を論理的に示す議論である。今回の形式証明は、Frey、Serre、Ribet、Wiles、Taylor–Wilesへ続く既知の数学と、Henri Darmon、Fred Diamond、Richard Taylorによる整理に沿っている。途中で多数の補題を明示的に証明していても、中心となる数学的経路は新しく考案されたものではない。

形式化は、その議論を証明支援系が解釈できる厳密な定義と推論へ変換する作業だ。人間には明白な型の一致や前提条件もコード上で埋める必要があり、論文を機械的に翻訳するだけでは終わらない。一方、形式化に必要な中間結果を新たに記述することと、定理に対する新しい数学的証明を発見することは区別しなければならない。

機械検証では、形式化された証明が採用した公理と論理規則のもとで成立するかをカーネルが判定する。これは言語モデルが文章を読んで「正しそうだ」と評価する確率的な処理とは異なる。ただし、形式化された命題が人間の意図した命題と一致しているか、中間定理の名称や説明が実際の内容を正しく伝えているかという意味上の確認は、人間側に残る。

約1,300万行は既存資産の上に築かれた

成果物はゼロから作られたクリーンルーム実装ではない。Anthropicの公開リポジトリ はLean 4とMathlibを土台とし、Frey、Serre、Ribet、Wiles、Taylor–Wilesの議論を採用しているほか、Imperial College LondonのFLTプロジェクトとflt-regularから取得・改変した素材を含む106ファイル、Mathlibの記述を再現した23ファイルを帰属文書に記載している。生成文書には2万9,511件の定理ページがあり、各定理のLean文、参照先、参照元、依存関係を確認できる。

既存資産の利用は形式化の価値を否定しない。現代数学の証明は先行研究に依存し、Leanでの形式化もMathlibなどの共有ライブラリを再利用して進めるのが一般的だからだ。ただし、約1,300万行をすべてClaudeが独創した数学と解釈するのは誤りである。評価すべき対象は、既存の数学と形式資産を統合し、不足する中間段階を補って、最終命題まで検査可能な形にしたことだ。

どこまで機械的に確認されたのか

公開物の標準ビルドは、最終定理がLeanの三つの標準公理だけに依存することを確認する。未完成部分を許容する「sorry」、追加公理、通常の検査を迂回する手段が証明パッケージに入り込んでいないことも検査対象だ。さらにComparatorを使い、証明した命題がMathlibで独立に記述されたフェルマーの最終定理と一致するかを照合している。

別経路の検査には、Rustで実装された独立系Leanカーネルのnanodaが使われた。公開された検証結果では、同じ環境から書き出した105万2,234件の宣言がエラーなく受理されている。これにより、生成コードが表面的に完成しているだけでなく、形式体系の規則に従って再生できることを複数の経路で確かめた。

それでも「機械検証済み」は、あらゆる前提から独立した絶対的保証を意味しない。Leanまたはnanodaのカーネル、比較ツール、実行環境が正しく動くことへの信頼は必要であり、形式化された命題と人間が意図した数学との対応も確認しなければならない。今回の成果が直接保証するのは、公開された命題が明示された公理と依存関係の範囲で形式的に導かれていることだ。

成果の現在地

公開コードは研究成果物と位置付けられ、通常のソフトウェアプロジェクトのような継続保守や外部からの貢献は受け付けていない。全体の再ビルドにはLean 4.33.1と指定されたMathlib環境が必要で、コード、証明経路、帰属情報、複数の検証手順を含む大規模な成果物となっている。

今回の到達点は、フェルマーの最終定理をもう一度「解いた」ことではない。既知の深い数学を、複数のAIエージェントが共有基盤上で分担し、端から端まで機械検証できる形式証明へ変換した点にある。今後の評価では、外部の数学者や形式手法研究者による再現と精査、別の大型証明でも同じ工程が安定して機能するか、人間向けの解説と巨大な機械向け成果物をどう対応させるかが焦点となる。