Anthropicのフェルマーの最終定理Lean証明を検証する方法

「Claudeがフェルマーの最終定理を解いた」という見出しを見かけたら、まず形式化したという言葉に注目してください。Anthropicは、定理を最初から最後まで検査できるとするLeanの成果物を公開しました。ただし、その中身は新しい証明の発見ではありません。使われているのは、Frey–Serre–Ribet–Wiles–Taylor-Wilesに連なる、すでに確立された数学的ルートです。

まずは2つの主張を切り分ける

狭い意味でいえば、答えはイエスです。Anthropicは、フェルマーの最終定理（FLT）をLean 4で形式化した公開リポジトリをリリースしており、ビルドと検証の手順も掲載しています。一方で、Claudeがこの有名な問題を独力で解決したという言い方は正確ではありません。数学的なブレークスルーをもたらしたのは、何十年も前のAndrew WilesとRichard Taylorです。

FLTは、n > 2のとき、a^n + b^n = c^nを満たす正の整数解が存在しないという定理です。Wilesの証明は1995年に発表され、今回の成果は、その確立済みの道筋を機械で検査できる成果物に落とし込んだものです。背景を知りたい場合は、Lean CommunityによるFLTプロジェクトの発表も参照してください。

Leanの証明が答えるのは、数学論文の非形式的な説明とは別の問いです。厳密にエンコードされた命題が、指定された環境にある検査済みの定義・依存関係・公理から導かれることは示せます。しかし、AIが基礎となる数学を発明したことや、定理名と実際の命題が一致していることまで証明するものではありません。

Anthropicが実際に公開したもの

Anthropicの2026年9月4日付の研究ブログによると、Claudeは11日間でFLTを完全かつエンドツーエンドにコンピューター検証できるLean形式化として生成しました。記事では、Leanのコードが約1,300万行、証明された定理文が30,300件、最終的な証明で使われたものが29,500件、さらに出力トークンが約60億に達したと説明されています。

この作業ではProve2Meが使われました。Anthropicによれば、これは定理文の有向非巡回グラフを管理し、複数のエージェントを調整するプラットフォームです。形式化の内容は、Frey、Serre、Ribet、Wiles、Taylor-Wilesに結び付く既存の証明ルートを簡略化して説明したものに沿っています。

主張を確認するうえでは、発表記事よりも公開されたGitHubリポジトリのほうが役に立ちます。デフォルトのターゲットはFinalCheck.leanで、定理の宣言は次のとおりです。

theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ)
  (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
  a ^ n + b ^ n ≠ c ^ n

リポジトリ自身が、研究用の成果物であり、保守されておらず、コントリビューションも受け付けていないと明記しています。Lean 4.33.1とMathlib v4.33.0に固定され、PROOF-PATH.mdも含まれています。定理と定義の依存関係を、オフラインで閲覧できるHTML形式の出力も用意されています。

リポジトリの最終チェックでは、追加された公理、sorry、native_decide、unsafeなどの抜け道に依存していた場合、失敗するよう設計されています。スクリーンショットや説明文を信じるだけでなく、成果物そのものを調べられる点が重要です。

再現可能な検証手順

本格的に確認するなら、別のプロジェクトに単独の.leanファイルをコピーするのではなく、まずリポジトリが固定している環境をそのまま使います。Lean Communityの検証ガイドが説明しているとおり、Leanは毎月リリースされ、Mathlibも頻繁に変更されるため、後方互換性が保証されていないからです。

ビルド前に環境を固定する

リポジトリによると、ビルドの対象環境はLinuxまたはmacOSで、elan、Git、Python、GNU coreutilsが必要です。Lakeが固定された依存関係を取得してビルドするため、ネットワーク接続も求められます。.lake以下だけで約67 GB、さらに生成されるCファイルにおよそ220 GB必要になるとされています。Cファイルは後から削除できます。

また、並列ジョブ1つにつき約5 GBのメモリが必要で、一部のモジュールでは最大36 GBを要すると報告されています。96ジョブで実行した場合、リポジトリ側のビルド実績は5時間32分、メモリ使用量のピークは153 GBでした。これは本記事で計測した値ではなく、リポジトリが報告している数字です。実行時間を保証するものではなく、必要なリソースを見積もる際の注意材料として捉えてください。

検証方法を選ぶ

• 読むだけ: ビルドせずにFinalCheck.lean、PROOF-PATH.md、ATTRIBUTION.mdを確認する。
• Leanでフルビルド: 固定されたツールチェーンを使い、lake buildを実行する。
• 独立した再実行: ビルドとエクスポートが終わったら、comparatorとnanodaのスクリプトを実行する。

新しくクローンした直後は、リポジトリが次のような手順を案内しています。

git clone https://github.com/anthropics/fermats-last-theorem.git flt
cd flt

# Lower the number if your machine cannot supply the required memory.
LEAN_NUM_THREADS=96 lake build

# Check the result against a Mathlib-only challenge statement.
verification/comparator/run.sh

# Run after the comparator check.
verification/nanoda/run.sh

各ステージの役割は異なります。

Comparatorは、定理文を読む代わりにはなりません。プロジェクトが、弱められた命題や微妙に異なる命題を証明していないか確認する助けになる仕組みです。リポジトリのPROOF-PATH.mdは、数学上の各ステップとLeanの宣言を対応付けています。生成されたHTMLページを使えば、Webアプリケーションを起動せずに依存関係を調べられます。

2つ目の検証には追加のリソースも必要です。リポジトリによると、37.8 GBのエクスポートファイルを書き出す際に約90 GBのメモリが必要になる場合があり、nanodaのチェック中には約40 GBが必要になることがあります。

証拠が示すこと、示せないこと

Lean Communityの「Did you prove it?」チェックリストが示す重要な原則は、コンパイルが検証するのはエンコードされた命題であって、定理名が意図した非形式的な主張と一致しているかどうかではない、ということです。今回の成果物では、ComparatorとMathlibの利用によってそのリスクは抑えられています。それでも、定理の宣言と証明の道筋を読む必要がなくなるわけではありません。

この成果物が示すこと、示さないこと

今回のシステムは、異例の規模で、Leanによる正式検証済みの成果物を生成しました。しかし、新しいFLTの証明ルートや、初等的な新証明、Claudeによる独立した数学的発見を示したわけではありません。

Anthropicは、この証明がWilesのルートを簡略化したものに沿っていると説明しています。リポジトリも既存研究への依存を明記しており、ATTRIBUTION.mdでは、Mathlibに加えて、Imperial College LondonのFLTプロジェクトまたはflt-regular由来の内容を含むファイルが106件あるとしています。この出自を踏まえることは、公開された成果物の正体を正確に説明するうえで欠かせません。

プロジェクトでは、実行中に30,300件の定理文が証明され、そのうち約29,500件が最終証明で使われたと報告されています。一方、リポジトリには29,511ページの定理があると記載されています。これらは形式化された宣言や依存関係の数であって、新たに発見された数学的成果が29,511件あるという意味ではありません。形式証明では、人間の証明なら専門家の理解に委ねられる暗黙のステップ、型、強制変換、定義、ライブラリ依存関係まで明示的に展開されます。

リポジトリは、ソースコードが読むためではなく、検査されるために書かれているとも説明しています。名前は機械生成で、P2Mのようなラベルはパイプライン上の分類にすぎず、権威を持つのは名前ではなく命題そのものです。だからこそ、見出しの定理だけでなく、証明経路とComparatorも確認する必要があります。

過去のLean研究を、2026年の主張にまとめてしまうのも適切ではありません。2023年のフェルマーの最終定理に関する論文は、正則素数に対するKummerの定理のCase Iを、完全かつsorryなしで形式化したと報告しました。一方で、Case IIとKummerの補題には大きな作業が残っているとも述べています。2025年の改訂版では、正則素数に関する形式化を、その限定されたケースについての完全な証明と説明しています。

Imperial/Lean FLTプロジェクトは、現代数論の形式化を、単一の定理を翻訳するだけではない、より広い基盤整備の取り組みとして説明しています。Anthropicの公開物は、既存の形式化エコシステムの中で、AIエージェントを協調させると何ができるのかを示す補足的な証拠と見るのが適切です。先行プロジェクトの目的が不要になったことを示すものではありません。

何をどこまで信頼すべきか

ニュースとして概要だけ知りたいなら、公式発表とリポジトリによってプロジェクトの存在は確認できます。監査が必要なら、固定された環境でビルドを再現し、定理文を確認してください。AI研究として評価するなら、オーケストレーション、既存ライブラリ、過去の形式化、計算資源まで含めてシステム全体を見る必要があります。

FAQ

Claudeはフェルマーの最終定理の新しい証明を発見したのですか？

いいえ。Anthropicの成果物は、Frey、Serre、Ribet、Wiles、Taylor-Wilesに連なる既存の証明ルートを形式化したものです。成果の中心は、機械で検査できるLean成果物を大規模かつ短期間で生成した点にあり、新しい数学的解法を見つけたことではありません。

Leanのビルドが成功すれば、非形式的な定理も証明されたことになりますか？

そのLean環境で検査された依存関係から、エンコードされた命題が導かれることは証明されます。ただし、その命題と定義が、自分が主張したい非形式的な定理に対応しているかどうかは、別途確認しなければなりません。

リポジトリはsorryや追加の公理を使っていますか？

リポジトリの説明では、最終チェックがsorry、追加の公理、native_decide、unsafeなど、複数のショートカットを拒否するとされています。想定される公理リストは、Lean標準の3つの公理であるpropext、Classical.choice、Quot.soundです。発表記事だけを信じず、実際にチェックを再現してください。

普通のノートパソコンで結果を再現できますか？

リポジトリの閲覧や一部のビルドはできるかもしれませんが、完全な検証は一般的な軽量タスクではありません。リポジトリの報告では、ビルド時のメモリ使用量のピークが153 GB、Comparatorでは最大230 GBに達し、ディスク容量も大きく必要になります。ハードウェアが大きな制約になる点には注意が必要です。

この主張を正確に確認するなら、まず環境を固定したGitHubの成果物を入手し、見出しより先に定理宣言を読んでください。そして結果は、既知の数学をAIが支援して形式化した大規模な成果物として報告するのが適切です。