AI開発企業のAnthropicは2026年9月4日、AI「Claude」がフェルマーの最終定理について最初から最後までコンピューターで検証できる証明を完成させたと発表しました。Claudeは11日間にわたってほぼ自律的に作業し、証明支援システム「Lean 4」で約1300万行のコードを生成。Anthropicはフェルマーの最終定理について初の完全な機械検証済み証明だと説明しています。

Formalizing Fermat's Last Theorem \ Anthropic

https://www.anthropic.com/research/formalizing-fermats-last-theorem





フェルマーの最終定理は「nが2より大きい整数の場合、aⁿ＋bⁿ＝cⁿを満たす正の整数a、b、cは存在しない」というもの。17世紀にフランスの数学者ピエール・ド・フェルマーが書き残して以来350年以上にわたって未解決でしたが、数学者のアンドリュー・ワイルズらが証明を完成させ、1995年に発表しました。ワイルズの証明は129ページに及び、正しさを確認する作業には数カ月かかりました。

数学の証明では論理のつながりが1カ所でも崩れると、その先の結論まで成立しなくなる可能性があります。人間向けの論文では読者にとって明らかな手順が省略されることがありますが、コンピューターに証明を確認させる場合は「明らか」とされる細かな手順まで厳密に記述する必要があります。既知の数学的証明を証明支援システムが確認できる形へ書き直す作業が「形式化」です。

インペリアル・カレッジ・ロンドンの数学者ケビン・バザード氏は2024年からフェルマーの最終定理をLeanで形式化する共同プロジェクトを率いており、初期段階の作業計画だけでも86ページに達しています。形式化には数年かかると見込まれていました。

Anthropicの研究者でAIによる数学の形式化を研究するティエンイー・ペン氏がClaudeに作業させたところ、Claudeは11日間で約3万300件の定理を機械検証できる形で証明し、最終的な証明では約2万9500件を使用しました。約1300万行という規模は、Lean向け数学ライブラリ「Mathlib」の5倍以上とのこと。数十のClaudeエージェントが概念の定義や中間定理の証明を分担し、より難しい命題の証明へ順番に進んでいきました。



ただし複数のAIを動かすだけで作業が進んだわけではなく、初期の試行では各エージェントが巨大なプロジェクトの進捗状況を把握できなくなり、互いの成果をうまく利用できなくなるなどのトラブルが発生しました。長期間にわたる複雑な作業では、AI自身の能力に加えて「どこまで終わったのか」「次に何を証明すべきなのか」を管理する仕組みが必要になるというわけです。

問題の解決に使われたのが、ペン氏らが開発した数学形式化用の共同作業プラットフォーム「Prove2Me」です。Prove2Meは定理同士の依存関係を有向非巡回グラフ(DAG)と呼ばれる構造で管理し、複数のClaudeが次に取り組むべき定理を確認できるようにしました。また定理の内容を記した部分と証明を別々のファイルに分けてコンパイルを高速化し、各定理に自然言語による説明を付けることで、すでに完成した証明を検索して再利用しやすくしています。



完成した証明はLeanによるチェックを通過し、GitHubで公開されています。証明はLeanの標準的な3つの公理だけに依存しており、未証明部分を一時的に通す「sorry」なども含まれていません。Mathlibに収録されているフェルマーの最終定理の記述と証明対象が一致することも比較ツールで確認済み。さらにRustで実装された独立したLeanカーネル「nanoda」でも100万件以上の宣言をエラーなしで検査できたと報告されています。

GitHub - anthropics/fermats-last-theorem · GitHub

https://github.com/anthropics/fermats-last-theorem

AIが数学の証明を大量に生み出せるようになるほど、人間だけで正しさを確認する負担も大きくなります。そのためAnthropicは今後、人間向けの論文とあわせてコンピューターで検証できる形式化済みの証明を作成することが一般的になると予想しているとのことです。