350年以上にわたって数学者を悩ませた「フェルマーの最終定理」。
Anthropicは9月4日、Claudeを使って、この定理を完全にコンピューターで検証できる形へ形式化したと発表しました。
かかった期間は11日。生成されたLeanコードは約1300万行で、最終的な証明では約2万9500件の中間定理が使われています。
ただし、ここには重要な注意点があります。
Claudeがフェルマーの最終定理の新しい数学的証明を発見したわけではありません。
すでに知られている証明を、コンピューターが論理の一段一段まで確認できる形式へ変換したのが今回の成果です。
「新しい証明」ではなく、既知の証明を機械が読める形へ
フェルマーの最終定理は、
「nが3以上の整数なら、aⁿ＋bⁿ＝cⁿを満たす正の整数a、b、cは存在しない」
という有名な定理です。
1637年ごろ、ピエール・ド・フェルマーが本の余白に書き残したことから始まり、最終的にはアンドリュー・ワイルズとリチャード・テイラーらの仕事によって1990年代に証明されました。
今回Claudeが行ったのは、それとは別の数学的アイデアを発見することではありません。
Anthropic自身も、今回新しいのは数学そのものではなくverification（検証）だと説明しています。
人間向けの数学論文では、
「既知の結果から従う」
「同様に示せる」
といった具合に、専門家なら補える論理を省略できます。
しかしLeanのような定理証明支援系では、その省略を基本的に許しません。
定義、中間定理、最終結論まで、機械が確認できる形で論理をつなぐ必要があります。
Claudeが取り組んだのは、いわば人間向けの数学を「コンピューターが一切忖度せず検算できるコード」へ変換する作業です。
129ページの証明が、なぜ1300万行になるのか
Anthropicは、ワイルズらによる証明を129ページと紹介しています。
1995年のAnnals of Mathematicsに掲載された論文を分けると、
- Andrew Wiles：109ページ
- Richard Taylor・Andrew Wiles：20ページ
の合計129ページです。
一方、Claudeが生成した形式化は約1300万行のLeanコードに達しました。
ただし、
129ページ → 1300万行だから約10万倍複雑
という比較はできません。
そもそもの目的が違います。
| 人間向けの数学論文 | Leanによる形式化 |
|---|---|
| 専門家が読む | コンピューターが検証する |
| 自明な手順は省略できる | 論理を細かく明示する |
| 過去の知識を暗黙に使える | 定義や定理を形式的につなぐ |
| 読みやすさを重視 | 機械検証できることを重視 |
Anthropic自身も、今回のコードは必要以上に長い可能性が高いとしています。
約1300万行という数字は、「フェルマーの最終定理には本来これだけ必要」という意味ではありません。
現在のAIが、非常に巨大なコードを使ってでも複雑な数学を最後まで形式化できたことを示す数字と見る方が正確です。
11日で約3万300件の定理、Claude単体の成果ではない
「Claudeが11日でやった」と聞くと、チャット画面へ問題を入力して待っていたようにも聞こえます。
実態はかなり違います。
Anthropicによると、数十のClaudeエージェントが並行して、
- 数学的な概念を定義する
- 中間定理を証明する
- 完成した定理を別の証明で再利用する
- 失敗した経路を別の方法で試す
といった作業を分担しました。
途中でコンピューター検証可能な形で証明した定理は約3万300件。そのうち最終的な証明で使われたものが約2万9500件です。
消費した出力トークンは約60億。
使用したのも一般利用者向けClaudeそのものではなく、Claude Fable 5.1とおおむね同等の社内研究モデルです。
この大規模な並列作業を成立させた重要な仕組みが「Prove2Me」でした。
Prove2Meは、証明すべき定理を依存関係のグラフとして管理します。
例えば、
Aを証明するにはBとCが必要
↓
BにはDが必要
↓
Dが完成したらBへ戻る
という構造を複数エージェントで共有できます。
今回の成果は、
高性能なAIモデル＋Lean＋Mathlib＋複数エージェント＋Prove2Me
を組み合わせて達成したものです。
「LLM単体が突然数学者になった」と理解するのは、少し実態と違います。
1300万行を人間が読まなくても検証できる
AIが1300万行も書いたなら、
「その1300万行が正しいことを誰が確認するのか」
という疑問も出てきます。
ここがLeanを使う大きな意味です。
Anthropicが公開したリポジトリによると、全6万475モジュールをLeanのカーネルでチェックしています。
最終的な定理はLeanの標準的な3つの公理だけに依存し、「sorry」のように証明を飛ばす仕組みも使っていません。
さらに、
- Lean本体
- comparator
- Rustで書かれた独立したLeanカーネル「nanoda」
という複数の方法で確認されています。
nanodaでは105万2234件の宣言をエラーなしで検証しました。
もちろん、Leanのカーネルやコンピューターそのものまで無限にさかのぼって証明できるわけではありません。
それでも、1300万行すべてを人間が目視するのではなく、比較的小さな検証システムへ論理チェックを集約できるのが形式証明の強みです。
数学者Kevin Buzzard氏も、Anthropicの公開コードを自身の環境でコンパイルし、comparatorによる確認を実施。
本人ブログ「FLT: Anthropic has beaten me to it」で、検証が通ったことを報告しています。
Buzzard氏自身もImperial College Londonでフェルマーの最終定理をLeanへ形式化するプロジェクトを進めており、5年間で100万ポンドの予算を得ています。
そのBuzzard氏は、今回の成果について、数学そのものに新しい知識を加えたものではないとしつつ、自動形式化の技術としては大きな前進だと評価しています。
Hacker Newsでは「証明したのか？」から検証コストまで議論
このニュースはHacker Newsでも大きな反応を集めています。
9月5日6時56分の確認時点で、関連投稿は333ポイント・213コメントでした。
議論では、
- これは新しい数学的証明なのか
- 1300万行ものAI生成コードをどう信用するのか
- Leanで検証できること自体が今回の意味ではないか
- 約60億出力トークンという計算量をどう見るか
- 人間だけなら同じ形式化にどれほど時間がかかるのか
といった論点が出ています。
特に、「formalizing（形式化）」と「discovering（新しい証明の発見）」の違いをどう捉えるかが、議論の中心の一つになっています。
11日という速さだけでなく、AIが作った数学をどう信頼するのかという問題にも関心が集まっています。
本当に大きいのは、これからAIが作る数学を検算できること
今回の成果で長期的に重要なのは、フェルマーの最終定理そのものではないかもしれません。
AIが今後、新しい数学的結果を大量に生み出すようになれば、人間側には別の問題が発生します。
誰が、それを全部チェックするのか。
非常に難しい数学論文では、正しさが広く受け入れられるまで何カ月、何年もかかることがあります。
AIが証明を作る速度だけ急速に上がれば、検証側が追いつきません。
そこで、
AIが数学を作る
↓
AIがLeanへ形式化する
↓
Leanが論理的な整合性を機械チェックする
↓
人間は数学的な意味や価値を評価する
という分業が成立すれば、状況は大きく変わります。
Anthropicも、AIが生成する数学が増えるほど、形式化が人間による査読負担を軽くする可能性を指摘しています。
Claudeが今回示したのは、「AIがフェルマーを解いた」という話ではありません。
既知の非常に複雑な数学を、AIが短期間で“機械が検算できる形”へ変換できるところまで来た。
こちらの方が、今回のニュースの本質に近そうです。
参照したネット反応
- Hacker News「Formalizing Fermat’s Last Theorem」 — 333ポイント・213コメント（2026年9月5日 6:56確認）
参照した一次情報
- 発表元：Anthropic
- 資料名：Formalizing Fermat’s Last Theorem
- 発表日または更新日：2026年9月4日
- 発表元：Anthropic
- 資料名：Fermat’s Last Theorem in Lean 4
- 発表日または更新日：日付表記なし
- 発表元：Annals of Mathematics
- 資料名：Modular elliptic curves and Fermat’s Last Theorem
- 発表日または更新日：1995年5月
- 発表元：Annals of Mathematics
- 資料名：Ring-theoretic properties of certain Hecke algebras
- 発表日または更新日：1995年5月
参考にした専門家コメント
- 発信者：Kevin Buzzard / Xena Project
- 記事名：FLT: Anthropic has beaten me to it
- 公開日：2026年9月4日
