物語 → 証明証明全体は、残る仕事を奇素数にしぼるところから始まります。ここがあとの章の枠組みにもなります。
事件の着地点theorem solution : FermatLastTheorem「なぜ？」から始まる、数学の冒険
小さな「なぜ？」。 大きな冒険。
物語を追い、証明に触れる。気になったら、もうひとつ奥まで。
アカウント不要。APIキー不要。好奇心だけで。
ふたつの入口。お茶の間は、ひとつ。
今日は数学と戦わないまんがから入ります:17章、64個の小石、必須の式はゼロ。Leanの原文は、訪ねてくるまでガラス越しです。
数学へまっすぐ証明マップから始めます:名付けられた定理が数千本。そして時計の逆元からR = Tまで、階段を全部登ります。となりでは物語も語り続け、あなたを正直に保ちます。
ふたりで読むために作りました:数学好きと、数学が苦手なひと。ソファは一台。それぞれが持ち帰ったものは、お茶の間へ運びます。
「まだわからない」から始めよう。
全17章で、ひとつの大きな道筋へ。今日は、小さな発見がひとつあれば十分。
全17章 · Lean元の原文 ↗
ピップの心得：まちがいも手がかり。どの章にも進めて、何度でも考え直せます。
累乗、問題の還元、あやしい小包。
証明全体のマップを開く29,511の定理・正確な主張・依存関係
英語や日本語で定理を検索できます。主要な定理には日本語の見出しがあります。文脈全体はGitHubの原文から確かめられます。
この章で見つけたいこと
いちばん小さな奇素数が、どんな勝利で閉じられるかを見よう。
- interval_cases
- 変数の範囲が有界であることを利用し、有限の候補を順に扱うタクティック。
- 読み込む定理
- 別のファイルにある名前つきの結果。ここで適用しても、主張を書き直す必要はありません。
元の原文 ↗ · L130–139固定版 aa2d8b3
theorem solution : FermatLastTheorem := by
apply FermatLastTheorem.of_odd_primes
intro p pp p_odd
by_cases hp5 : 5 ≤ p
· exact FreyPackage.fermatLastTheoremFor_of_five_le p pp hp5
· have hp2 := pp.two_le
interval_cases p
· exact absurd p_odd (by decide)
· exact fermatLastTheoremThree
· exact absurd pp (by decide)
編集はこのタブに残ります。漫画は元の原文の説明なので、行との対応は一時停止しています。FLT全体をこのサイトで検証することはできません。
👩🏻🎨 ミカ · 原文を読むための案内
apply FermatLastTheorem.of_odd_primesで残る仕事は奇素数だけになります。intro p pp p_oddが素数と証拠を割り当て、by_cases hp5 : 5 ≤ pが分岐します。負の枝ではhp2 := pp.two_leがinterval_casesを支え、有界な候補p = 2・3・4を列挙します。二つの不可能はabsurdで死に、生き残ったp = 3は読み込みの一行exact fermatLastTheoremThreeで閉じます。
元の原文への注釈・Leanの実行状態ではありませんコマの手がかりや原文の色つきの語句に触れると、対応をたどれます。
この論理を試してみる →出典と検証の範囲
出典：anthropics/fermats-last-theorem（aa2d8b3）。上流では検証済みと報告されていますが、このアプリでは全体を再ビルド・再検証していません。漫画の解説自体は形式的な証明ではありません。
ソースのライセンスと著作者表示第2章／全17章・Lean
三の場合の事件簿
折りたためない紙は、専用のフォルダを要求します。
ここまでと、この先
第1章の主張は、3以上のすべての指数についてでした。この章ではn = 3を別に扱います。階段の話のように、一つの場合と他の場合を扱う仕組みは役割が違います。この一件だけで全体が終わるわけではありません。
このつながりは、読む道筋の案内です。物語のたとえ自体が、この定理の証明になるわけではありません。
まず、この言葉から
知っている言葉は飛ばして大丈夫。初めてなら、言葉を開くか、基礎から順に読んでみよう。
- 9を法とする三乗三乗は、9の時計では0・1・8のどれかに落ちます。三の場合の物語の最初の一歩です。
- 単元つきのより広い網降下のために、単元uのかかったもっと大きな主張を、まず証明します。
- いちばん小さい解を選ぶ仮の解を、λがcを割る回数で順位づけると、いちばん小さいものが必ずあります。
- アイゼンシュタインの世界の三つの因子1の原始3乗根が入った世界では、三乗の和が三つの因子に分かれます。
- 必ず終わる階段必ず小さくなる目盛りは、小さくなり続けられません。フルマーの降下法です。
ミカ
「指数3は、この機械よりずっと昔に自分のフォルダを手に入れました。」
二つの出口、一つの生還者物語 → 証明指数5以上は小包とともに出発します。三の場合だけが机の上に残ります。
5以上は小包の道へexact FreyPackage.fermatLastTheoremFor_of_five_le p pp hp5ピップ
「しぼったあと残るのは、3と4だけのとても短いリスト。」
とても短いリスト物語 → 証明interval_casesは、証明された範囲の中での候補の列挙です。無限の探索ではなく、有限の確認です。
有界な列挙interval_cases p物語 → 証明一行の読み込みが、数百年前の降下法を現代の証明へ運びます。古い勝利は今も使える数学です。
オイラーの降下法を読み込むfermatLastTheoremThree物語の向こうにある考え方
apply FermatLastTheorem.of_odd_primesで残る仕事は奇素数だけになります。intro p pp p_oddが素数と証拠を割り当て、by_cases hp5 : 5 ≤ pが分岐します。負の枝ではhp2 := pp.two_leがinterval_casesを支え、有界な候補p = 2・3・4を列挙します。二つの不可能はabsurdで死に、生き残ったp = 3は読み込みの一行exact fermatLastTheoremThreeで閉じます。
最後の枝でinterval_casesが列挙する候補は？
- p = 2・3・4。2と4が落ちて、3が生き残る。
- 自然数を一つずつ、全部。
このページで物語と原文を読めます。証明の編集、クイズ、対話式のマップにはJavaScriptを有効にしてください。
練習用のリアルタイム検査
証明の続きを、あなたの手で。
小さな場面、本物の論理の目標。そして、あなたの成功を気にかけるハト。
事件簿を開いています…