2026年9月、AnthropicはClaudeがフェルマーの最終定理をLeanで形式化し、端から端までコンピューターで検証できる証明を完成させたと発表しました。
ただし、「Claudeがフェルマーの最終定理を新しく証明した」と受け取ると内容が変わってしまいます。
フェルマーの最終定理そのものは、Andrew WilesとRichard Taylorらの仕事によって1990年代に証明済みです。今回Claudeが行ったのは、既存の数学的証明をLeanという証明支援系で1ステップずつ確認できる形へ書き直す「形式化」です。
それでも成果の規模は大きく、Anthropicによると、数十体のClaudeエージェントが11日間で約1,300万行のLeanコードを書き、30,300件の中間定理を証明しました。最終証明では約29,500件が使われています。
この記事では、「新しい証明」と「形式化」の違い、Leanが何を確認したのか、Prove2Meがなぜ重要だったのか、今回の成果が今後のAI研究に何を変えるのかを2026年9月11日時点の情報から見ていきます。
Claudeがしたのは「新しい証明の発見」ではなく既存証明の形式化
フェルマーの最終定理は、整数nが2より大きいとき、
a^n + b^n = c^n
を満たす正の整数a、b、cは存在しない、という定理です。
この定理は長く未解決でしたが、Wilesの研究とTaylorとの修正を経て1995年に正しい証明が公表されました。
今回のClaudeの仕事は、そこから新しい証明方法を発見したものではありません。
Anthropicの形式化は、Frey、Serre、Ribet、Wiles、Taylor-Wilesへ続く既存の議論を、Darmon・Diamond・Taylorによる解説に沿ってLeanへ落とし込んだものです。
違いを短くすると、次のようになります。
| 内容 | 今回のClaude |
|---|---|
| フェルマーの最終定理そのものを初めて証明 | していない |
| Wilesらとは別の新しい証明を発見 | していない |
| 既存証明をLeanで形式化 | 行った |
| 証明をコンピューターで端から端まで検証可能にした | 行った |
| 公開された形式化を第三者が再検証できる | できる |
「既に証明済みなら意味が薄い」という話でもありません。
人間向けの数学論文では、読者が補える当然の手順や過去研究の結果を省略できます。一方、Leanは論理のつながりを機械的に確認するため、必要な定義や中間定理を明示しなければ先へ進めません。
複雑な現代数学を、その厳密さのまま機械が検証できる形へ変換する作業自体が大きな仕事です。
Leanは「文章がもっともらしいか」ではなく論理の接続を確認する
Leanは、数学者の文章を読んで妥当そうか判断するAIではありません。
定理、定義、仮定、証明手順を形式言語で記述し、それぞれの論理的なつながりを小さなカーネルが確認します。
今回公開されたリポジトリでは、最終的なフェルマーの最終定理がLean 4で定義され、ビルド時に証明全体がLeanカーネルによって検査されます。
さらにAnthropicの公開リポジトリでは、
- Lean 4.33.1で全体をビルド
- Mathlib v4.33.0を基盤として使用
- 追加の未証明公理や
sorryを使わないことを確認 - Mathlib側のフェルマーの最終定理の定義と一致するか比較
- Rustで書かれた別実装のLeanカーネル「nanoda」でも再確認
という複数の検証手順が用意されています。
つまり、「Claudeが正しいと言っているから正しい」のではなく、Claudeが出力した形式証明を別の検証機構がチェックする構造です。
この点が、通常の生成AIによる数学回答とは大きく違います。
11日で約1,300万行、30,300件の中間定理
Anthropicが公表した規模はかなり大きなものです。
- 作業期間：約11日
- Leanコード：約1,300万行
- 証明した中間定理：約30,300件
- 最終証明で使われた中間定理：約29,500件
- 使用した出力トークン：約60億
- 実行モデル：Claude Fable 5.1とおおむね同等と説明される社内研究モデル
ここで「Claude Fable 5.1が単独で11日間考え続けた」と捉えるのも正確ではありません。
実際には、Claude Codeベースのマルチエージェント構成で、数十体のエージェントが概念定義、中間定理、既存結果の探索などを並列に進めました。
大きな成果を出した要因は、モデル単体の性能だけではなく、多数のAIが同じ証明全体を壊さず分担できる作業基盤にあります。
Prove2Meが複数AIの作業をつないだ
今回の形式化で重要な役割を果たしたのが、Columbia UniversityのDAPLabなどが開発する「Prove2Me」です。
初期の試行では、複数エージェントが大規模な証明へ同時に取り組むと、
- どの中間定理が終わったのか追えない
- 同じ定理を別のAIが重複して証明する
- 長時間の作業で前提や依存関係を見失う
- 1つの変更が別の証明を壊す
といった問題が起きました。
Prove2Meは、証明全体を定理の依存関係でつないだグラフとして管理します。
各AIは巨大な証明全体を常に記憶しておくのではなく、「今どの定理を証明すれば先へ進めるか」を共有された依存グラフから判断できます。
さらに、
- 定理文と証明を分離して管理
- 依存関係を追跡
- 複数エージェントが並列作業
- 自然言語で既存定理を検索
- 既に証明済みの結果を再利用
- Leanによる自動検証
といった仕組みを持ちます。
これは数学に限らず、長時間動くAIエージェント全般へ通じる考え方です。
1体のAIへ巨大な仕事を丸ごと渡すより、仕事を小さく分け、依存関係と完了状態を外部システムで管理した方が、長い作業を安定して進めやすくなります。
人間が積み上げた数学ライブラリも大きく使っている
今回の成果をClaudeだけの力として見るのも正確ではありません。
公開リポジトリは、Leanの数学ライブラリMathlibに加え、Imperial College LondonでKevin Buzzardらが進めてきたフェルマーの最終定理の形式化プロジェクトや、別の形式化プロジェクトの成果を利用しています。
AnthropicのATTRIBUTIONファイルでは、公開リポジトリ内の106ファイルについて、ImperialのFLTプロジェクトやflt-regular由来の素材が含まれることを明示しています。
つまり今回の成果は、
- Wilesらによる元の数学的証明
- 数学者による解説・体系化
- LeanとMathlib
- 既存の形式化プロジェクト
- Prove2Me
- Claudeの複数エージェント
が積み重なって成立したものです。
AIが人間の過去研究を置き換えたというより、人間が長年作ってきた形式化資産の上で、AIが非常に大きな変換作業を短期間に進めたと見る方が実態に近いです。
「機械検証済み」でも人間向けの説明は不要にならない
形式証明には、人間が読む数学論文とは別の強みがあります。
コンピューターが論理の抜けを細かく確認できるため、AIが大量の数学的成果を生成する時代には、結果の検証手段として重要になります。
一方、1,300万行の機械生成Leanコードを数学者が最初から最後まで読むのは現実的ではありません。
公開リポジトリ自身も、このLeanコードは「読むため」より「検証するため」に作られており、名称なども機械生成されたものだと説明しています。
そのため今後は、
- 人間が理解するための数学的説明
- Leanなどによる機械検証可能な形式証明
を両方用意する形が増えていきそうです。
Anthropicも、形式証明が人間向けの説明を置き換えるのではなく、AIが生み出す研究成果を数学界が確認するための手段になるとしています。
公開された証明は自分でも再検証できるが、かなり重い
形式証明はGitHubで公開されており、ソース自体は確認できます。
ただし、全体を手元で再ビルドする作業は軽くありません。
Anthropicが公開している再検証例では、60,000を超えるモジュールをビルドし、高並列環境でも数時間を要しています。比較検証ではさらに長い時間と大容量メモリが必要です。
そのため、一般的なPCで気軽に数分試すタイプのデモではありません。
一方、Prove2Meそのものは現在オープンな共同形式化プラットフォームとして公開されており、人間やAIエージェントが小さな定理・ミッション単位で参加できます。
フェルマーの最終定理と同じ巨大プロジェクトを自宅PCで再現する必要はなく、仕組み自体はより小さな課題でも利用できます。
今回の成果で重要なのは「AIが答えた」より「AIの答えを検証できる」こと
生成AIが数学で強くなると、「難しい問題へ答えられるか」に目が向きます。
今回の形式化では、もう一段別の変化が見えます。
AIが大量の中間結果を作ったとしても、それを人間がすべて目視で確認するのは難しくなります。そこで、AI自身に形式言語を書かせ、証明支援系のカーネルに検証させる方法が重要になります。
流れとしては、
- AIが証明候補を作る
- Leanへ形式化する
- カーネルが論理を検証する
- 人間は証明の意味や価値、前提を確認する
という役割分担です。
AI研究が速くなるほど、「AIが何を出したか」だけでなく、その成果を機械的に検証できる形で残せるかが重要になります。
フェルマーの最終定理の形式化は、その規模が一気に大きくなった例として見る価値があります。
まとめ
Claudeが2026年9月に完成させたのは、フェルマーの最終定理の新しい数学的証明ではありません。
Wilesらによる既存の証明をもとに、Leanで端から端までコンピューターが確認できる形式証明へ変換した成果です。
それでも、約1,300万行・約3万件の中間定理からなる巨大な形式化を、Prove2Meと複数のClaudeエージェントで11日間にまとめた意味は小さくありません。
今回見えてきたのは、AIが数学を「答える」だけでなく、大量の研究成果を検証可能な形式へ変換する役割です。
今後AIが新しい定理や研究成果を大量に生み出すようになれば、Leanのような形式検証と、Prove2Meのように複数AIを協調させる基盤は、研究成果を信頼するための重要なインフラになっていきます。
