ピップ
「ぼくの整理法より古いファイル。どうりで整理されている。」
古いからこそ物語 → 証明古い引き出しは先行する証明の保管場所。ここでの候補は指数5・7・13に限られています。
三つの候補P.p = 5 ∨ P.p = 7 ∨ P.p = 13「なぜ？」から始まる、数学の冒険
小さな「なぜ？」。 大きな冒険。
物語を追い、証明に触れる。気になったら、もうひとつ奥まで。
アカウント不要。APIキー不要。好奇心だけで。
ふたつの入口。お茶の間は、ひとつ。
今日は数学と戦わないまんがから入ります:17章、64個の小石、必須の式はゼロ。Leanの原文は、訪ねてくるまでガラス越しです。
数学へまっすぐ証明マップから始めます:名付けられた定理が数千本。そして時計の逆元からR = Tまで、階段を全部登ります。となりでは物語も語り続け、あなたを正直に保ちます。
ふたりで読むために作りました:数学好きと、数学が苦手なひと。ソファは一台。それぞれが持ち帰ったものは、お茶の間へ運びます。
「まだわからない」から始めよう。
全17章で、ひとつの大きな道筋へ。今日は、小さな発見がひとつあれば十分。
全17章 · Lean元の原文 ↗
ピップの心得：まちがいも手がかり。どの章にも進めて、何度でも考え直せます。
曲線の算術を、勝手に切り分けられない理由。
証明全体のマップを開く29,511の定理・正確な主張・依存関係
英語や日本語で定理を検索できます。主要な定理には日本語の見出しがあります。文脈全体はGitHubの原文から確かめられます。
この章で見つけたいこと
昔の数学の成果が、大きな証明の道具になることを知ろう。
- absurd
- 命題の証拠とその否定から、任意の結論を導く。
- 選言
- A ∨ Bのように、複数の可能性のどれかが成り立つという命題。
元の原文 ↗ · L25–29固定版 aa2d8b3
theorem solution (P : FreyPackage) (hp : P.p = 5 ∨ P.p = 7 ∨ P.p = 13) : ¬ HasGaloisStableCofixedLine (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p := by
rcases hp with h | h | h
· exact absurd h (P.p_ne_of_fermatLastTheoremFor_K fermatLastTheoremFive)
· exact absurd h (P.p_ne_of_fermatLastTheoremFor_K fermatLastTheoremSeven)
· exact absurd h (P.p_ne_of_fermatLastTheoremFor_K fermatLastTheoremThirteen)
編集はこのタブに残ります。漫画は元の原文の説明なので、行との対応は一時停止しています。FLT全体をこのサイトで検証することはできません。
👩🏻🎨 ミカ · 原文を読むための案内
rcases hp with h | h | hで指数の等式を3つの場合に分けます。補助定理はFermatLastTheoremFor nとP.hFLTからP.p≠nを得ます。absurd hで等式とその否定をぶつけるため、直線の仮定を導入する必要もありません。
元の原文への注釈・Leanの実行状態ではありませんコマの手がかりや原文の色つきの語句に触れると、対応をたどれます。
この論理を試してみる →出典と検証の範囲
出典：anthropics/fermats-last-theorem（aa2d8b3）。上流では検証済みと報告されていますが、このアプリでは全体を再ビルド・再検証していません。漫画の解説自体は形式的な証明ではありません。
ソースのライセンスと著作者表示まず、この言葉から
知っている言葉は飛ばして大丈夫。初めてなら、言葉を開くか、基礎から順に読んでみよう。
- 素数2以上で、正の約数が1と自分自身だけの数。
- 偶数・奇数と場合分け数を偶数と奇数に分けるのは、この証明そのものが使う最初の場合分けです。
- 仮の反例とフライ小包ないはずの解を仮に置き、数と条件の証拠をまとめます。
- 同じ対象についての矛盾同じfについて、f ≠ 0とf = 0の証拠は両立しません。
- 四乗は二乗にたためる四乗は正方形の正方形です。それで指数4の場合は、一つ下の指数の等式にたためます。
- 事件簿の等式をいちどに束ねるFermat42が容疑者にいちど名前をつけます:非ゼロのa・bとa⁴ + b⁴ = c²。
- また、いちばん小さい容疑者を選ぶFermat42の解を|c|で順位づけると、いちばん小さいバッジが必ずあります。
- 容疑者の内側の二つの直角三角形ピタゴラス数の分類が、a⁴ + b⁴ = c²をより小さい平方のつらなりへ変えます。
- もっと小さい容疑者が現れるm・r・sはみな平方数になり、|i| < |c|の新しい解が矛盾を呼びます。
ミカ
「ここでの候補は5・7・13の三つだけ。それぞれのファイルを開こう。」
場合を分けよう物語 → 証明三つのファイルの山は∨で結ばれた三つの選択肢。rcasesで、一つずつ証明の枝を開きます。
一つずつ場合分けrcases hp with h | h | hピップ
「5は証明済みの結果を借りられるね。小さくなる解とお昼休みの冗談は、奥の話です。」
5の出番物語 → 証明小さくなる箱は降下法のイメージ。この抜粋では降下法を再演せず、証明済みの指数5の定理を使います。
5の場合の定理を使うfermatLastTheoremFiveミカ
「7と13にも証明済みの結果があるよ。残りのファイルも閉じられるね。」
勝利を借りる物語 → 証明閉じたファイルを借りるのは、証明済みの結果を再利用すること。指数13の定理で、残りの枝の一つを閉じます。
13の場合の定理を使うfermatLastTheoremThirteen物語の向こうにある考え方
rcases hp with h | h | hで指数の等式を3つの場合に分けます。補助定理はFermatLastTheoremFor nとP.hFLTからP.p≠nを得ます。absurd hで等式とその否定をぶつけるため、直線の仮定を導入する必要もありません。
この抜粋だけでクンマーの定理を最初から証明している？
- いいえ。その証明に依存する結果を使っている。
- はい。rcasesが理論全体を含んでいる。
このページで物語と原文を読めます。証明の編集、クイズ、対話式のマップにはJavaScriptを有効にしてください。
練習用のリアルタイム検査
証明の続きを、あなたの手で。
小さな場面、本物の論理の目標。そして、あなたの成功を気にかけるハト。
事件簿を開いています…