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/フォルダは証明全体をオフラインで閲覧できるウェブページとして提示します（下記「ブラウザで証明を読む」参照）。 研究成果物。メンテナンスされておらず、貢献は受け付けていません。 ステートメント Theorems/Thm_fermat_last_theorem.leanは、定理 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、追加公理なし、native_decideなし）に正確に基づいている場合を除き、ビルドは失敗します。 FinalCheck.leanは、Mathlib独自のステートメントであるFermatLastTheoremもこの定理から導出します。 検証方法 ビルド。 Lean 4.33.1（2026カーネルの健全性修正を含む）でのスクラッチからのlakeビルド。Mathlibはソースからコンパイルされます。 このリポジトリの60,475モジュールすべてがビルドされ、各宣言はLeanカーネルによってチェックされ、公理は上記の通りです。 comparator.leanprover/comparator v4.33.0は、verification/comparator/Challenge.leanでステートメントをMathlibのみを使用して記述したビルドと比較しました。 証明されたステートメントとそれが言及するすべての定数がチャレンジと同一であること、他の公理が使用されていないこと、そしてMathlib全体を含む証明全体がLeanカーネルでリプレイされることを確認しました。 判定：あなたのソリューションはOKです！ セカンドカーネル。 nanoda 0.4.13は、Rustで書かれた独立したLeanカーネルで、同じ環境のエクスポート（lean4exportで作成）を受け入れました。 エラーなしで1052234の宣言をチェックしました。 私たちはnanodaに4つの小さなパッチ（verification/nanoda/patches/）を適用してビルドしました。1つは進捗出力を追加し、3つは定義的等価性検索を高速化します。これがないと、この証明のいくつかの宣言は、変更されていないnanodaでそれぞれ数時間かかります。 パッチのいずれも、タイピングルールを追加、削除、または弱めるものではありません。 モジュールには、axiom、sorry、native_decide、unsafe、extern、implemented_by、partial def、または#evalは含まれていません（Challenge.leanは意図的にsorryを使用しており、パッケージの一部ではありません）。 これらのチェックを組み合わせることで、上記のステートメントが、Leanカーネル（またはnanoda）とチェックツールの信頼性を前提として、3つの公理から導出されることが確立されます。 ステートメントはLeanの組み込み自然数、+、≤、<、≠を使用して書かれています。Mathlibの唯一の成分はℕ上の^であり、MathlibはこれをLeanの組み込みべき乗として定義しており、comparatorはステートメントが言及するすべての定義が標準Mathlibのものと同一であることをチェックします。 Mathlibの他の部分は信頼する必要はありません。なぜなら、カーネルはステートメントの下にあるすべてをチェックするからです。 ツールがチェックできないのは、各中間定理がその名前が示唆する意味を持っているかどうかです。これは読者が判断するものであり、PROOF-PATH.mdは各ステップの背後にあるLean定理の名前を示し、ここで証明された各名前付き古典結果の正確な強度を述べています。 ブラウザで証明を読む html/フォルダ（約390MB）は、このリポジトリを静的ウェブページとして提示します。 証明のルートをステップバイステップで表示します。 29,511の定理（正確なLeanステートメント、参照しているもの、参照されているもの、および展開可能な依存関係グラフ）と1,450の定義モジュール（完全なソースとそれを使用するステートメント）ごとのページ。 すべての定理と定義名に対する検索ボックス。 ランドマーク定理をグラフとして表示。 README.md、PROOF-PATH.md、ATTRIBUTION.mdをクロスリンク付きでレンダリング。 このフォルダはリポジトリの一部であるため、クローンまたはZIPダウンロードにはすでに含まれています（html/を別のアーカイブとして取得した場合は、リポジトリのルートに展開してください）。 ウェブブラウザでhtml/index.htmlを開いてください。すべてオフラインで、Webサーバーなしで動作します。 ページはChromiumベースのブラウザでのみ機械的にテストされ、html/README-DOCS.mdはLeanファイルから引用されたものと生成されたもの（英語の要約と推奨参照は自動生成され、Leanステートメントが権威があります）を説明しています。 自分でチェックする LinuxまたはmacOSが必要です（一部のパスはWindowsでは長すぎます）。elan（lean-toolchainからLean 4.33.1をインストールします）。ネットワーク接続が必要です。 LakeはMathlibをGitHubから取得し、ソースからコンパイルします。このツールチェーンに一致する事前ビルドされたMathlibはないためです（96ジョブで約13分）。 ビルドには、並列ジョブあたり約5GBのメモリが必要です（一部のモジュールは最大36GB必要です）。.lake/の下に約67GBのディスク容量、およびビルド中に削除できるCファイル（約220GB）が必要です。 私たちのビルドは96ジョブで5時間32分かかり、ピークメモリは153GBでした。 comparatorは約15時間かかります（私たちのビルド：14時間46分）。そのほとんどはシングルコアでのカーネルリプレイです。 ピークメモリは230GBだったので、300GBを確保してください。 comparatorスクリプトの後にnanodaを実行します。そのツールは再利用されます。 37.8GBのエクスポートの書き込みには約90GBのメモリが1時間かかり、チェック自体には約40GB（16スレッドで約30分）かかります。 両方のスクリプトはLinux用です（bash、git、python3、GNU coreutils; nanodaはpatch、cargo、crates.ioも必要です）。 ```bash git clone <this repository> flt && cd flt LEAN_NUM_THREADS=96 lake build # デフォルトではハードウェアスレッドごとに1つのジョブ。メモリを制限するために低くしてください（ジョブあたり約5GB） 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/には前述のウェブページ、tools/docs-site/にはそれらを生成したプログラムが含まれています。 Leanソースは、人間が書いたオープンソースLeanを基盤とするAIエージェントによって生成され、Leanが調停者として機能します。読みやすさよりもチェックしやすさを重視して書かれています。名前は機械生成され、P2Mや16進数サフィックスのようなラベルは数学ではなくパイプラインラベルです。名前とステートメントが一致しない場合は、ステートメントが証明されたものです。 コメントは、アップストリームの通知、ドキュメント文字列、および引用（ATTRIBUTION.mdにリストされている）と、#guard_msgsがチェックする期待出力コメントを除いて削除されました。 ライセンスと帰属表示 Copyright 2026 Anthropic, PBC; Apache License 2.0（LICENSE）の下でリリースされました。 一部は、Kevin Buzzard率いるImperial College London FLTプロジェクト（Freyパッケージ、Galois表現、変形理論、パッチングなど）、flt-regular（Kummerの定理）、およびMathlibから派生した3つのApache-2.0プロジェクトに由来します。 ATTRIBUTION.mdは、最初の2つからの素材を含む106ファイル、著作権所有者と著者、およびMathlibテキストを再証明する23ファイル（Definitions/Def_Compat_Mathlib430.leanの抜粋と、Mathlibの補題を再証明する22モジュール）をリストしています。 ウェブページは、KaTeXとGraphviz（WebAssemblyにコンパイル）を独自のライセンスの下でバンドルしています。これらはhtml/assets/vendor/LICENSES.txtにリストされています。 Leanとlake-manifest.jsonのパッケージはビルド時に取得され、ここでは配布されません。 帰属表示のない素材を認識した場合、その省略は意図的ではありません。