物語 → 証明三つの袋の共通のリボンは共通因子。余分な荷物を除き、最大公約数が1の反例を目指します。
共通の荷物を整理Int.gcd a b = 1「なぜ？」から始まる、数学の冒険
小さな「なぜ？」。 大きな冒険。
物語を追い、証明に触れる。気になったら、もうひとつ奥まで。
アカウント不要。APIキー不要。好奇心だけで。
ふたつの入口。お茶の間は、ひとつ。
今日は数学と戦わないまんがから入ります:17章、64個の小石、必須の式はゼロ。Leanの原文は、訪ねてくるまでガラス越しです。
数学へまっすぐ証明マップから始めます:名付けられた定理が数千本。そして時計の逆元からR = Tまで、階段を全部登ります。となりでは物語も語り続け、あなたを正直に保ちます。
ふたりで読むために作りました:数学好きと、数学が苦手なひと。ソファは一台。それぞれが持ち帰ったものは、お茶の間へ運びます。
「まだわからない」から始めよう。
全17章で、ひとつの大きな道筋へ。今日は、小さな発見がひとつあれば十分。
全17章 · Lean元の原文 ↗
ピップの心得：まちがいも手がかり。どの章にも進めて、何度でも考え直せます。
累乗、問題の還元、あやしい小包。
証明全体のマップを開く29,511の定理・正確な主張・依存関係
英語や日本語で定理を検索できます。主要な定理には日本語の見出しがあります。文脈全体はGitHubの原文から確かめられます。
この章で見つけたいこと
反例を簡単な形にしても、大事な条件を失わない理由を知ろう。
- obtain
- 存在する対象と、それが条件を満たす証拠を取り出す。
- rflのパターン
- 等式の証拠を分解しながら、その等式で置き換える。
元の原文 ↗ · L17–29固定版 aa2d8b3
have ⟨a, b, c, a0, b0, c0, ab, H⟩ :
∃ (a b c : ℤ), a ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0 ∧ Int.gcd a b = 1 ∧ a ^ p + b ^ p = c ^ p := by
obtain ⟨d, a', b', d0, cop, a_eq, b_eq⟩ :=
Int.exists_gcd_one' (Int.gcd_pos_of_ne_zero_left b ha)
simp only [a_eq, mul_pow, b_eq] at H
rw [← add_mul, mul_comm] at H
obtain ⟨c', rfl⟩ := (Int.pow_dvd_pow_iff pp.ne_zero).1 ⟨_, H.symm⟩
rw [mul_pow] at H
have a0' := left_ne_zero_of_mul (a_eq ▸ ha)
have b0' := left_ne_zero_of_mul (b_eq ▸ hb)
have c0' := right_ne_zero_of_mul hc
exact ⟨a', b', c', a0', b0', c0', cop,
mul_left_cancel₀ (pow_ne_zero _ (mod_cast d0.ne')) H⟩
編集はこのタブに残ります。漫画は元の原文の説明なので、行との対応は一時停止しています。FLT全体をこのサイトで検証することはできません。
👩🏻🎨 ミカ · 原文を読むための案内
obtainでInt.exists_gcd_one'の証拠を取り出し、mul_powで共通のp乗因子を露わにします。Int.pow_dvd_pow_iffからc′を得ます。最後のmul_left_cancel₀には、消去する冪が非零だという証拠を渡します。
元の原文への注釈・Leanの実行状態ではありませんコマの手がかりや原文の色つきの語句に触れると、対応をたどれます。
この論理を試してみる →出典と検証の範囲
出典：anthropics/fermats-last-theorem（aa2d8b3）。上流では検証済みと報告されていますが、このアプリでは全体を再ビルド・再検証していません。漫画の解説自体は形式的な証明ではありません。
ソースのライセンスと著作者表示第4章／全17章・Lean
小包のダイエット
ピップは傘を3本。式は共通因子を持ち込んだ。
ここまでと、この先
指数を絞ったので、次は仮の数の組を整理します。天秤で「何を保つ操作か」を確かめたように、式を保つことが大切。ここでは共通の因子にも注意します。
このつながりは、読む道筋の案内です。物語のたとえ自体が、この定理の証明になるわけではありません。
まず、この言葉から
知っている言葉は飛ばして大丈夫。初めてなら、言葉を開くか、基礎から順に読んでみよう。
この章を基礎から順に説明して →ミカ
「剥がしましょう——小さい解が下に潜っています。三つとも割れば、gcd 1まで届きます。」
割るときは慎重に物語 → 証明リボンを外しても中身は残します。割り切れることの定理で、aとbだけでなくcも因数分解できると確かめます。
割れる理由を確かめるInt.pow_dvd_pow_iff物語 → 証明袋ごと捨てると証拠も消えます。非零の補題によって、小さくした数も0ではないと確かめます。
非零の証拠を残すright_ne_zero_of_mul hcミカ
「軽くなったかばんも、ぴったり閉まる:約分のあとも等式は無事。証拠はきちんと整えてこそ証拠です。」
証拠はそのまま物語 → 証明軽くなったかばんにも等式は残ります。共通因子が0ではないという証拠を使って、約分を正当化します。
証拠つきで約分mul_left_cancel₀物語の向こうにある考え方
obtainでInt.exists_gcd_one'の証拠を取り出し、mul_powで共通のp乗因子を露わにします。Int.pow_dvd_pow_iffからc′を得ます。最後のmul_left_cancel₀には、消去する冪が非零だという証拠を渡します。
最後の組で示していることは？
- フェルマーの最終定理全体。
- 仮定Hのもとで、互いに素な反例が存在すること。
このページで物語と原文を読めます。証明の編集、クイズ、対話式のマップにはJavaScriptを有効にしてください。
練習用のリアルタイム検査
証明の続きを、あなたの手で。
小さな場面、本物の論理の目標。そして、あなたの成功を気にかけるハト。
事件簿を開いています…