ピップ
「石を三つ、小包へ:a・b・c、禁止された等式から直送です。サンドイッチは型についての一回きりの冗談。」
証拠専用のかばん物語 → 証明三つの石は整数a・b・cの役。サンドイッチの冗談は、入れられるものに型の条件があることを表します。
小包に入る整数a : ℤ「なぜ？」から始まる、数学の冒険
小さな「なぜ？」。 大きな冒険。
物語を追い、証明に触れる。気になったら、もうひとつ奥まで。
アカウント不要。APIキー不要。好奇心だけで。
ふたつの入口。お茶の間は、ひとつ。
今日は数学と戦わないまんがから入ります:17章、64個の小石、必須の式はゼロ。Leanの原文は、訪ねてくるまでガラス越しです。
数学へまっすぐ証明マップから始めます:名付けられた定理が数千本。そして時計の逆元からR = Tまで、階段を全部登ります。となりでは物語も語り続け、あなたを正直に保ちます。
ふたりで読むために作りました:数学好きと、数学が苦手なひと。ソファは一台。それぞれが持ち帰ったものは、お茶の間へ運びます。
「まだわからない」から始めよう。
全17章で、ひとつの大きな道筋へ。今日は、小さな発見がひとつあれば十分。
全17章 · 物語元の原文 ↗
ピップの心得：まちがいも手がかり。どの章にも進めて、何度でも考え直せます。
累乗、問題の還元、あやしい小包。
証明全体のマップを開く29,511の定理・正確な主張・依存関係
英語や日本語で定理を検索できます。主要な定理には日本語の見出しがあります。文脈全体はGitHubの原文から確かめられます。
この章で見つけたいこと
仮の数の組を、条件の証拠を持つ数学的な対象に変えてみよう。
- 証拠つきのデータ
- 数だけでなく、その数が条件を満たす証明も一緒に持つこと。
元の原文 ↗ · L17–38固定版 aa2d8b3
structure FreyPackage where
a : ℤ
b : ℤ
c : ℤ
ha0 : a ≠ 0
hb0 : b ≠ 0
hc0 : c ≠ 0
p : ℕ
pp : Nat.Prime p
hp5 : 5 ≤ p
hFLT : a ^ p + b ^ p = c ^ p
hgcdab : gcd a b = 1
ha4 : (a : ZMod 4) = 3
hb2 : (b : ZMod 2) = 0
編集はこのタブに残ります。漫画は元の原文の説明なので、行との対応は一時停止しています。FLT全体をこのサイトで検証することはできません。
👩🏻🎨 ミカ · 原文を読むための案内
この店は、禁止された等式を小包に変えます。石は整数a・b・c。封は、指数が素数で5以上という証拠。梱包はgcd 1を記録します。台車が運ぶのは証拠の欄——形式的な証明では、証拠のない設計図は何も組み立てないからです。
元の原文への注釈・Leanの実行状態ではありませんコマの手がかりや原文の色つきの語句に触れると、対応をたどれます。
この論理を試してみる →出典と検証の範囲
出典：anthropics/fermats-last-theorem（aa2d8b3）。上流では検証済みと報告されていますが、このアプリでは全体を再ビルド・再検証していません。漫画の解説自体は形式的な証明ではありません。
ソースのライセンスと著作者表示第5章／全17章・物語
あやしい小包
反例が1つ。添付書類は山ほど。
ここまでと、この先
前章で仮の数の組と条件を整えました。今度は、その材料から曲線を作ります。直角三角形の話でも数と図を結びましたが、ここは別の高度な構成です。同じ定理を使っているわけではありません。
このつながりは、読む道筋の案内です。物語のたとえ自体が、この定理の証明になるわけではありません。
まず、この言葉から
知っている言葉は飛ばして大丈夫。初めてなら、言葉を開くか、基礎から順に読んでみよう。
- 仮の反例とフライ小包ないはずの解を仮に置き、数と条件の証拠をまとめます。
- ワイエルシュトラスの標準形ここで使う曲線は、五つの係数で決まる標準の形に整えます。
- 等式から曲線へ禁止された等式が、ワイエルシュトラス曲線の具体的な係数を与えます。
- 分数と有理数割り算は分数を残すことがあります。分数を含む数の世界が有理数ℚです。
- 共通因子と互いに素互いに素とは、1より大きな正の共通の約数がないこと。
- 方程式で決まる曲線方程式を満たす座標の組を集めたものが、ここでの曲線です。
物語 → 証明封を点検するのは小包の条件を確かめること。指数が素数で、5以上という証拠も必要です。
素数にも下限があるhp5 : 5 ≤ p物語 → 証明整えた装置は正規化したデータのたとえ。最大公約数が1という欄が、共通因子を除いたことを記録します。
正規化した小包hgcdab : gcd a b = 1ミカ
「うちの台車が運ぶのは証拠の欄であって、希望ではありません。Leanでは、証拠のない設計図は何も梱包しません。」
仮定つきの配達物語 → 証明台車の書類は構造が要求する証拠。設計図を定義しただけでは、反例の小包が実在することにはなりません。
設計図には証拠が必要structure FreyPackage where物語の向こうにある考え方
この店は、禁止された等式を小包に変えます。石は整数a・b・c。封は、指数が素数で5以上という証拠。梱包はgcd 1を記録します。台車が運ぶのは証拠の欄——形式的な証明では、証拠のない設計図は何も組み立てないからです。
FreyPackageという型を定義したら、反例もできる？
- いいえ。必要な数と条件の証拠をそろえないと作れない。
- はい。名前をつければ反例が存在する。
このページで物語と原文を読めます。証明の編集、クイズ、対話式のマップにはJavaScriptを有効にしてください。
練習用のリアルタイム検査
証明の続きを、あなたの手で。
小さな場面、本物の論理の目標。そして、あなたの成功を気にかけるハト。
事件簿を開いています…