Lean 4におけるフェルマーの最終定理

Lean 4におけるフェルマーの最終定理

Lean 4 を用いたフェルマーの最終定理の完全な機械検証済み証明です。これは Mathlib（Lean 4.33.1、Mathlib v4.33.0、lakefile.lean でコミットによりピン留め）上に構築されています。証明の論法は、Frey、Serre、Ribet、Wiles、Taylor-Wiles のものです。PROOF-PATH.md は各ステップとそれを担うLeanの定理を命名しており、html/ フォルダは証明全体をオフラインで閲覧可能なWebページとして提示しています（下記「ブラウザでの証明の読み方」参照）。

これはリサーチ成果物であり、メンテナンスされておらず、貢献も受け付けていません。

ステートメント

Theorems/Thm_fermat_last_theorem.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

そして、デフォルトのビルドターゲット FinalCheck.lean には以下が含まれています。

/-- info: 'fermat_last_theorem' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms fermat_last_theorem

そのため、証明がLeanの標準的な3つの公理のみに依存している場合（sorry、追加のaxiom、native_decideなし）でなければ、ビルドは失敗します。FinalCheck.lean は、この定理からMathlib自身のステートメント FermatLastTheorem も導出します。

検証方法

• ビルド。 Lean 4.33.1（2026カーネルの健全性修正を含む）でスクラッチから lake build を実行し、Mathlibはソースからコンパイルしました。このリポジトリの60,475モジュールすべてがビルドされ、各宣言はLeanカーネルによってチェックされ、公理は上記のとおりです。
• comparator。 leanprover/comparator v4.33.0 は、Mathlibのみを使用して定理をステートする verification/comparator/Challenge.lean に対してビルドをチェックしました。証明されたステートメントとそれが言及するすべての定数がチャレンジと同一であること、他の公理が使用されていないこと、そして証明全体（Mathlibを含む）がLeanカーネルでリプレイされることを確認しました。結果: Your solution is okay!
• セカンドカーネル。 nanoda 0.4.13、Rustで書かれた独立したLeanカーネルは、同じ環境のエクスポート（lean4exportで記述）を受け入れました: Checked 1052234 declarations with no errors。私たちは4つの小さなパッチ（verification/nanoda/patches/）を適用してnanodaをビルドしました。1つは進捗出力を追加し、3つは定義的等価性検索を高速化します。これらがないと、この証明のいくつかの宣言は、変更されていないnanodaでそれぞれ数時間かかります。パッチはいずれも、型付け規則を追加、削除、または弱めるものではありません。

モジュールには axiom、sorry、native_decide、unsafe、extern、implemented_by、partial def、または #eval は含まれていません（Challenge.lean は設計上 sorry を使用しており、パッケージの一部ではありません）。

これらのチェックを組み合わせることで、上記のステートメントが3つの公理から導出されることが確立されます。これは、Leanカーネル（またはnanoda）とチェックツールの信頼性を前提としています。ステートメントは、Leanの組み込み自然数、+、≤、<、≠ を使用して記述されています。Mathlibの唯一の要素は、ℕ上の^であり、これはMathlibがLeanの組み込みべき乗として定義しており、comparatorはステートメントが言及するすべての定義が標準Mathlibのものと同一であることをチェックします。これ以下のすべてはカーネルがチェックするため、Mathlibの他の部分は信頼する必要はありません。どのツールもチェックできないのは、各中間定理がその名前が示唆する意味を持っているかどうかです。これは読者の判断に委ねられ、PROOF-PATH.md は各ステップの背後にあるLean定理を命名し、各名前付き古典結果がここで証明されている強さを正確に述べています。

ブラウザでの証明の読み方

ドキュメントは Documentation Website でホストされています。リポジトリの html/ フォルダからローカルでも閲覧できます。手順は以下の通りです。

html/ フォルダ（約390 MB）は、このリポジトリを静的Webページとして提示します。証明の経路をステップバイステップで表示し、29,511の定理それぞれ（正確なLeanステートメント、それが引用するもの、およびそれを引用するもの、展開可能な依存関係グラフ）、および1,450の定義モジュールそれぞれ（完全なソースコードとそれを使用するステートメント）のページがあります。すべての定理名と定義名の検索ボックス、ランドマーク定理のグラフ、およびクロスリンク付きでレンダリングされた README.md、PROOF-PATH.md、ATTRIBUTION.md も含まれます。このフォルダはリポジトリの一部であるため、クローンまたはZIPダウンロードには既に含まれています（html/ を別アーカイブとして取得した場合は、リポジトリのルートに展開してください）。html/index.html をWebブラウザで開けば、すべてオフラインで、Webサーバーなしで動作します。ページはChromiumベースのブラウザでのみ機械テストされており、html/README-DOCS.md にはLeanファイルから引用されたものと生成されたもの（英語の要約と推奨参照は自動生成され、Leanステートメントが権威となります）が説明されています。

ご自身でチェックする

• LinuxまたはmacOS（一部のパスはWindowsでは長すぎるため）、elan（Lean 4.33.1を lean-toolchain からインストールします）、およびネットワーク接続が必要です。LakeはMathlibをGitHubから取得しソースからコンパイルします。なぜなら、このツールチェーンに一致する事前ビルド済みMathlibが存在しないためです（96ジョブで約13分）。
• ビルドには、並列ジョブあたり約5 GBのメモリが必要です（一部のモジュールは最大36 GB必要）。.lake/ 以下に約67 GBのディスク容量、およびビルド中に削除可能なCファイル（約220 GB）が必要です。私たちの環境では、96ジョブで5時間32分かかり、ピークメモリ使用量は153 GBでした。
• comparatorは約15時間かかります（私たちの環境: 14時間46分）。そのほとんどはシングルコアでのカーネルリプレイです。ピークメモリ使用量は230 GBだったので、300 GBを確保してください。nanodaはcomparatorスクリプトの後に実行し、そのツールを再利用します。37.8 GBのエクスポート作成には約90 GBのメモリが1時間かかり、チェック自体は約40 GB（16スレッドで約30分）かかります。両方のスクリプトはLinux用です（bash、git、python3、GNU coreutils; nanodaは patch、cargo、crates.ioも必要です）。

git clone <this repository> flt && cd flt
LEAN_NUM_THREADS=96 lake build              # デフォルトではハードウェアスレッドごとに1ジョブ。メモリを制限するために低くしてください（ジョブあたり約5 GB）
verification/comparator/run.sh              # 判定: .verify-work/wrapper/comparator.log の最終行
verification/nanoda/run.sh                  # comparatorスクリプトの後; 判定: .verify-work/nanoda/run-*/nanoda.stdout

Leanはビルド中に多数の非推奨およびスタイルリンター警告を出力しますが、結果には影響しません。ビルドが成功したかどうかは、出力が'flt_mathlib' depends on axioms: [propext, Classical.choice, Quot.sound]とBuild completed successfullyで終わることで確認できます。各スクリプトは、ピン留めされたバージョンでチェッカーを取得してビルドし、成功時に終了コード0を返します。

ソースについて

FinalCheck.lean がデフォルトターゲットです。Theorems/ にはステートメント、P2M/Sol/ には証明（引用するステートメントをインポート）、Definitions/ には定義、verification/ には2つのチェック、html/ には前述のWebページ、tools/docs-site/ にはそれらを生成したプログラムが含まれています。Leanソースは、人間が書いたオープンソースのLeanを基盤とし、Leanを調停者としてAIエージェントによって生成され、読みやすさよりもチェックしやすさを重視して書かれています。名前は機械生成され、P2M や16進数サフィックスのようなラベルは数学的なものではなくパイプラインラベルであり、名前とステートメントが一致しない場合はステートメントが証明されたものです。コメントは、アップストリームの通知、ドキュメント文字列、および引用（ATTRIBUTION.md にリストされています）と、#guard_msgs がチェックする期待出力コメントを除き、削除されています。

ライセンスと帰属

Copyright 2026 Anthropic, PBC; Apache License 2.0（LICENSE）の下で公開されています。一部は、Kevin Buzzard率いるImperial College London FLT project（Freyパッケージ、Galois表現、変形理論、パッチングなど）、flt-regular（Kummerの定理）、およびMathlibの3つのApache-2.0プロジェクトから派生しています（NOTICEでクレジットされています）。ATTRIBUTION.md は、最初の2つからの素材を含む106ファイル（アップストリームファイル、著作権所有者、著者）と、Mathlibのテキストを再証明する22モジュール（Definitions/Def_Compat_Mathlib430.lean の抜粋と、Mathlibの補題をその場で再証明する22モジュール）をリストしています。Webページは、KaTeXとGraphviz（WebAssemblyにコンパイル済み）を独自のライセンス（html/assets/vendor/LICENSES.txt にリスト）の下でバンドルしています。Leanおよびlake-manifest.jsonのパッケージはビルド時に取得され、ここで配布されるものではありません。帰属表示のない素材に気づいた場合、その省略は意図したものではありません。