物語 → 証明ピップのはさみは「分けられるのでは？」という提案。証明では可約性を一時的に仮定し、矛盾を探します。
分けられると仮定by_contra hred「なぜ？」から始まる、数学の冒険
小さな「なぜ？」。 大きな冒険。
物語を追い、証明に触れる。気になったら、もうひとつ奥まで。
アカウント不要。APIキー不要。好奇心だけで。
ふたつの入口。お茶の間は、ひとつ。
今日は数学と戦わないまんがから入ります:17章、64個の小石、必須の式はゼロ。Leanの原文は、訪ねてくるまでガラス越しです。
数学へまっすぐ証明マップから始めます:名付けられた定理が数千本。そして時計の逆元からR = Tまで、階段を全部登ります。となりでは物語も語り続け、あなたを正直に保ちます。
ふたりで読むために作りました:数学好きと、数学が苦手なひと。ソファは一台。それぞれが持ち帰ったものは、お茶の間へ運びます。
「まだわからない」から始めよう。
全17章で、ひとつの大きな道筋へ。今日は、小さな発見がひとつあれば十分。
全17章 · 物語元の原文 ↗
ピップの心得：まちがいも手がかり。どの章にも進めて、何度でも考え直せます。
曲線の算術を、勝手に切り分けられない理由。
証明全体のマップを開く29,511の定理・正確な主張・依存関係
英語や日本語で定理を検索できます。主要な定理には日本語の見出しがあります。文脈全体はGitHubの原文から確かめられます。
この章で見つけたいこと
「既約」とは、すべての対称性で保たれる非自明な部分空間がないことだと知ろう。
元の原文 ↗ · L77–91固定版 aa2d8b3
private theorem mazurM3asmB_of_no_cofixed (P : FreyPackage) :
GaloisRepIsIrreducible (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p := by
by_contra hred
have hN : HasGaloisStableCofixedLine (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p :=
rcases mazurM3asmB_exponent_trichotomy P.p P.pp P.hp5 with hsmall | h11 | h17
· exact FreyPackage.frey_no_cofixed_small P hsmall hN
· exact FreyPackage.frey_no_cofixed_eleven P h11 hN
· exact FreyPackage.frey_no_cofixed_large P h17 hN
theorem solution (P : FreyPackage) :
GaloisRepIsIrreducible (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p := by
rcases em ((P.a : ZMod 8) = 3) with h8 | _
· exact FreyPackage.Mazur_Frey_of_a_mod_eight P h8
· exact mazurM3asmB_of_no_cofixed P
編集はこのタブに残ります。漫画は元の原文の説明なので、行との対応は一時停止しています。FLT全体をこのサイトで検証することはできません。
👩🏻🎨 ミカ · 原文を読むための案内
主張:この対称性の結び目には、ほどける糸が一本もありません——どのシャッフルも触らない直線が存在しないのです。糸の存在を仮定するのは、間違っているけれど役に立つ手です。出口は一つずつ閉められ:小さい素数のドア、大きい素数のドア、そして最後に「直線は存在しない」の議論。可約性は自壊します。
元の原文への注釈・Leanの実行状態ではありませんコマの手がかりや原文の色つきの語句に触れると、対応をたどれます。
この論理を試してみる →出典と検証の範囲
出典：anthropics/fermats-last-theorem（aa2d8b3）。上流では検証済みと報告されていますが、このアプリでは全体を再ビルド・再検証していません。漫画の解説自体は形式的な証明ではありません。
ソースのライセンスと著作者表示まず、この言葉から
知っている言葉は飛ばして大丈夫。初めてなら、言葉を開くか、基礎から順に読んでみよう。
- 変換としての対称性形や計算の規則を保ったまま、対象を入れ替える変換。
- 行列という変換二行二列の数の表が変換を表し、行列どうしの掛け算もできます。
- ベクトルと部分空間足し算と数倍のできる対象。部分空間はその計算で外へ出ません。
- ガロア表現数の計算を保つ対称性を、ベクトルの変換として記録します。
- 既約性すべての対称性で保たれる部分空間は、0だけか全体だけ。
物語 → 証明独立して残る一本の線が、ガロア作用で保たれる直線の役。絵はその役割のたとえで、直線の数学的定義ではありません。
禁止された安定な直線HasGaloisStableCofixedLine物語 → 証明閉じられた出口は、その直線が存在できない素数の場合。ここで使う定理が、大きな素数の出口を閉じます。
大きな素数の出口を閉じるFreyPackage.frey_no_cofixed_large物語 → 証明切れずに残る丸は既約性という結論。残る場合にも、安定な直線がないという議論を使います。
直線がない議論を使うmazurM3asmB_of_no_cofixed物語の向こうにある考え方
主張:この対称性の結び目には、ほどける糸が一本もありません——どのシャッフルも触らない直線が存在しないのです。糸の存在を仮定するのは、間違っているけれど役に立つ手です。出口は一つずつ閉められ:小さい素数のドア、大きい素数のドア、そして最後に「直線は存在しない」の議論。可約性は自壊します。
既約とは、曲線の絵をハサミで切れないこと？
- はい。図形の切り方の規則です。
- いいえ。対称性で保たれる線形な部分についての性質です。
このページで物語と原文を読めます。証明の編集、クイズ、対話式のマップにはJavaScriptを有効にしてください。
練習用のリアルタイム検査
証明の続きを、あなたの手で。
小さな場面、本物の論理の目標。そして、あなたの成功を気にかけるハト。
事件簿を開いています…