物語 → 証明入場証は半安定性の証拠。笛への情熱では、必要な仮定を埋められません。
半安定という入場条件hW : W.IsSemistableModel「なぜ？」から始まる、数学の冒険
小さな「なぜ？」。 大きな冒険。
物語を追い、証明に触れる。気になったら、もうひとつ奥まで。
アカウント不要。APIキー不要。好奇心だけで。
ふたつの入口。お茶の間は、ひとつ。
今日は数学と戦わないまんがから入ります:17章、64個の小石、必須の式はゼロ。Leanの原文は、訪ねてくるまでガラス越しです。
数学へまっすぐ証明マップから始めます:名付けられた定理が数千本。そして時計の逆元からR = Tまで、階段を全部登ります。となりでは物語も語り続け、あなたを正直に保ちます。
ふたりで読むために作りました:数学好きと、数学が苦手なひと。ソファは一台。それぞれが持ち帰ったものは、お茶の間へ運びます。
「まだわからない」から始めよう。
全17章で、ひとつの大きな道筋へ。今日は、小さな発見がひとつあれば十分。
全17章 · Lean元の原文 ↗
ピップの心得：まちがいも手がかり。どの章にも進めて、何度でも考え直せます。
モジュラー性、3–5の切り替え、つながる部品。
証明全体のマップを開く29,511の定理・正確な主張・依存関係
英語や日本語で定理を検索できます。主要な定理には日本語の見出しがあります。文脈全体はGitHubの原文から確かめられます。
この章で見つけたいこと
難しい道具の細部を学ぶ前に、モジュラー性を示す作戦をつかもう。
- haveI
- 後の型クラス推論に使う局所インスタンスを登録する。
- resolve_left
- A∨Bと¬AからBを得る。
元の原文 ↗ · L165–180固定版 aa2d8b3
theorem modularity_of_semistableModel' (W : WeierstrassCurve ℤ) (hΔ : W.Δ ≠ 0)
(hW : W.IsSemistableModel) : (W.map (Int.castRingHom ℚ)).IsModular := by
by_cases h3 : W.ModRepIsIrreducible 3
·
obtain ⟨M₃, hM₃, hres₃, hcube₃, hns₃⟩ :=
isResiduallyModular_three_and_noInertiaFixedTorsion_and_not_cube_dvd_of_isSemistableModel W hΔ hW h3
haveI : NeZero M₃ := ⟨hM₃.ne'⟩
exact isModular_map_of_mlc1
(liftingAtConductor_three_of_level_hns 3 rfl W hΔ hW h3 M₃ hres₃ hns₃ hcube₃)
·
have h5 : W.ModRepIsIrreducible 5 := (modThreeOrFiveIrreducible W hΔ hW).resolve_left h3
obtain ⟨W', hΔ', hW', h3', hcong⟩ := threeFiveSwitchCurve W hΔ hW h5
編集はこのタブに残ります。漫画は元の原文の説明なので、行との対応は一時停止しています。FLT全体をこのサイトで検証することはできません。
👩🏻🎨 ミカ · 原文を読むための案内
by_cases h3でW.ModRepIsIrreducible 3を分けます。肯定側ではobtainでレベルと条件を取り出し、haveIでNeZero M₃を登録します。否定側ではresolve_left h3で5側の既約性を取り出します。切り替え後の議論はファイルの後半へ続きます。
元の原文への注釈・Leanの実行状態ではありませんコマの手がかりや原文の色つきの語句に触れると、対応をたどれます。
この論理を試してみる →出典と検証の範囲
出典：anthropics/fermats-last-theorem（aa2d8b3）。上流では検証済みと報告されていますが、このアプリでは全体を再ビルド・再検証していません。漫画の解説自体は形式的な証明ではありません。
ソースのライセンスと著作者表示まず、この言葉から
知っている言葉は飛ばして大丈夫。初めてなら、言葉を開くか、基礎から順に読んでみよう。
- 余りで比べる・合同数が違っていても、割った余りが同じなら合同です。
- 時計の算術余りの集合を決め、その中だけで計算する世界を作ります。
- 既約性すべての対称性で保たれる部分空間は、0だけか全体だけ。
- 半安定性素数ごとに余りの世界へ移したときの曲線のふるまいを制限します。
- 残余モジュラー性余りの世界へ移した算術データが、形式の係数と一致すること。
- 持ち上げ追加条件のある定理で、余りの情報から元の豊かな情報へ進みます。
物語 → 証明三つの点の入口は、3を法とする既約性の枝。条件がそろえば残余モジュラー性と持ち上げを使えます。
3の入口を調べるby_cases h3ピップ
「3の入口が閉まった。5の入口からなら進める？」
二つ目の入口物語 → 証明3の入口が閉じるのは最初の条件が成り立たない場合。resolve_leftで、二択の定理から5の条件を取り出します。
もう一方の入口へ(modThreeOrFiveIrreducible W hΔ hW).resolve_left h3物語 → 証明助っ人の入場証は、存在定理が保証する性質。適当な別の曲線を連れてきても使えません。
条件に合う助っ人threeFiveSwitchCurve物語の向こうにある考え方
by_cases h3でW.ModRepIsIrreducible 3を分けます。肯定側ではobtainでレベルと条件を取り出し、haveIでNeZero M₃を登録します。否定側ではresolve_left h3で5側の既約性を取り出します。切り替え後の議論はファイルの後半へ続きます。
by_cases h3は何を作る？
- h3が成り立つ枝と、その否定が成り立つ枝。
- 難しい場合を無視するための選択。
このページで物語と原文を読めます。証明の編集、クイズ、対話式のマップにはJavaScriptを有効にしてください。
練習用のリアルタイム検査
証明の続きを、あなたの手で。
小さな場面、本物の論理の目標。そして、あなたの成功を気にかけるハト。
事件簿を開いています…