物語 → 証明旅のあとにも残る石は、レベル下げで得られる非零の形式。レベル2・重さ2の空間に到着しています。
レベル2に非零の来客level_lowering_to_two P (frey_isModular P) hirr「なぜ？」から始まる、数学の冒険
小さな「なぜ？」。 大きな冒険。
物語を追い、証明に触れる。気になったら、もうひとつ奥まで。
アカウント不要。APIキー不要。好奇心だけで。
ふたつの入口。お茶の間は、ひとつ。
今日は数学と戦わないまんがから入ります:17章、64個の小石、必須の式はゼロ。Leanの原文は、訪ねてくるまでガラス越しです。
数学へまっすぐ証明マップから始めます:名付けられた定理が数千本。そして時計の逆元からR = Tまで、階段を全部登ります。となりでは物語も語り続け、あなたを正直に保ちます。
ふたりで読むために作りました:数学好きと、数学が苦手なひと。ソファは一台。それぞれが持ち帰ったものは、お茶の間へ運びます。
「まだわからない」から始めよう。
全17章で、ひとつの大きな道筋へ。今日は、小さな発見がひとつあれば十分。
全17章 · 物語元の原文 ↗
ピップの心得：まちがいも手がかり。どの章にも進めて、何度でも考え直せます。
レベルを下げ、空の部屋を開け、事件を解決する。
証明全体のマップを開く29,511の定理・正確な主張・依存関係
英語や日本語で定理を検索できます。主要な定理には日本語の見出しがあります。文脈全体はGitHubの原文から確かめられます。
この章で見つけたいこと
f≠0とf＝0が、どうして矛盾するのかを追ってみよう。
- 矛盾
- 同じ主張とその否定が両方導かれてしまうこと。
元の原文 ↗ · L139–147固定版 aa2d8b3
theorem Wiles_Frey (P : FreyPackage) :
¬ GaloisRepIsIrreducible (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p := fun hirr =>
let ⟨f, hf⟩ := level_lowering_to_two P (frey_isModular P) hirr
end FreyPackage
theorem solution (P : FreyPackage) : False :=
FreyPackage.Wiles_Frey P (FreyPackage.Mazur_Frey P)
編集はこのタブに残ります。漫画は元の原文の説明なので、行との対応は一時停止しています。FLT全体をこのサイトで検証することはできません。
👩🏻🎨 ミカ · 原文を読むための案内
最後の展示:事件全体を渡ってきて、なお非ゼロだった石——レベル下げが運び込んだ重さ2・レベル2の形式です。そのとなりには認定済みの空の箱:同じ空間の形式はすべてゼロという定理。同じ空間、同じ形式、二つの証明書。一方を他方に適用するのが、記録上もっとも速い矛盾です。運び役が消えれば、小包のルートは溶けます。
元の原文への注釈・Leanの実行状態ではありませんコマの手がかりや原文の色つきの語句に触れると、対応をたどれます。
この論理を試してみる →出典と検証の範囲
出典：anthropics/fermats-last-theorem（aa2d8b3）。上流では検証済みと報告されていますが、このアプリでは全体を再ビルド・再検証していません。漫画の解説自体は形式的な証明ではありません。
ソースのライセンスと著作者表示第16章／全17章・物語
入れないはずの客
ゼロではない客と、全員ゼロになる部屋。
ここまでと、この先
一方はf ≠ 0、他方は同じ空間でf = 0でした。両方は成り立ちません。第1章で仮に置いた解へ戻り、「その解が存在する」という仮定を退けます。
このつながりは、読む道筋の案内です。物語のたとえ自体が、この定理の証明になるわけではありません。
まず、この言葉から
知っている言葉は飛ばして大丈夫。初めてなら、言葉を開くか、基礎から順に読んでみよう。
- 導手とレベル下げ注意すべき素数を記録し、証明済みの条件でレベルの素因子を制限します。
- カスプ形式モジュラー形式に、すべての尖点で0へ近づく条件を加えたもの。
- 誰もいない部屋ある重さとレベルの空間では、すべてのカスプ形式が0だと定理で示します。
- 同じ対象についての矛盾同じfについて、f ≠ 0とf = 0の証拠は両立しません。
司書
「となりの箱は認定済みの空:同じ空間の形式はすべてゼロ。ほかの部屋の話は、いたしません。」
厳密な定員規則物語 → 証明空の展示箱は、同じ空間のすべての形式が0という定理。他の空間まで空だとは言っていません。
同じ形式がゼロになるModularForm.S2_Gamma0_2_eq_zeroミカ
「石と箱は同じ住所を共有します。非ゼロの証拠をゼロ定理の中に適用する——記録上もっとも速い終わり方。」
ありえない来客物語 → 証明空の箱の横にある石は、同じfについてのf ≠ 0とf = 0の証拠。hfを適用して矛盾を得ます。
非零とゼロがぶつかるhf物語 → 証明小包が消えるのは、モジュラー性と既約性の結果でフライ小包を排除したから。反例から小包への道も閉じます。
二つの結果から矛盾へFreyPackage.Wiles_Frey P (FreyPackage.Mazur_Frey P)物語の向こうにある考え方
最後の展示:事件全体を渡ってきて、なお非ゼロだった石——レベル下げが運び込んだ重さ2・レベル2の形式です。そのとなりには認定済みの空の箱:同じ空間の形式はすべてゼロという定理。同じ空間、同じ形式、二つの証明書。一方を他方に適用するのが、記録上もっとも速い矛盾です。運び役が消えれば、小包のルートは溶けます。
なぜf＝0とf≠0から矛盾する？
- 同じfについて、主張とその否定を得たから。
- ゼロという数が嫌われているから。
このページで物語と原文を読めます。証明の編集、クイズ、対話式のマップにはJavaScriptを有効にしてください。
練習用のリアルタイム検査
証明の続きを、あなたの手で。
小さな場面、本物の論理の目標。そして、あなたの成功を気にかけるハト。
事件簿を開いています…