ピップ
「今夜、私の舞台は無音です。出演者は一人もいない:定理によれば、この空間の形式はすべてゼロ。」
拍手の準備物語 → 証明静かな舞台は、この空間のどの形式も0という結論。奏者を見つけられなかっただけではありません。
どの形式もゼロになるf = 0「なぜ？」から始まる、数学の冒険
小さな「なぜ？」。 大きな冒険。
物語を追い、証明に触れる。気になったら、もうひとつ奥まで。
アカウント不要。APIキー不要。好奇心だけで。
ふたつの入口。お茶の間は、ひとつ。
今日は数学と戦わないまんがから入ります:17章、64個の小石、必須の式はゼロ。Leanの原文は、訪ねてくるまでガラス越しです。
数学へまっすぐ証明マップから始めます:名付けられた定理が数千本。そして時計の逆元からR = Tまで、階段を全部登ります。となりでは物語も語り続け、あなたを正直に保ちます。
ふたりで読むために作りました:数学好きと、数学が苦手なひと。ソファは一台。それぞれが持ち帰ったものは、お茶の間へ運びます。
「まだわからない」から始めよう。
全17章で、ひとつの大きな道筋へ。今日は、小さな発見がひとつあれば十分。
全17章 · 数学元の原文 ↗
ピップの心得：まちがいも手がかり。どの章にも進めて、何度でも考え直せます。
レベルを下げ、空の部屋を開け、事件を解決する。
証明全体のマップを開く29,511の定理・正確な主張・依存関係
英語や日本語で定理を検索できます。主要な定理には日本語の見出しがあります。文脈全体はGitHubの原文から確かめられます。
この章で見つけたいこと
形式が見つからないのではなく、すべてゼロになると証明する違いを知ろう。
- 部分群の指数
- 周囲の群における部分群の剰余類の個数。
- ノルムの構成
- ここでは、形式をより大きな群に対する形式へ移す構成。
元の原文 ↗ · L195–206固定版 aa2d8b3
theorem S2_Gamma0_2_eq_zero' (f : CuspForm (CongruenceSubgroup.Gamma0 2) 2) : f = 0 := by
have hweight : (2 : ℤ) * Nat.card ((↑(CongruenceSubgroup.Gamma 1) : Subgroup (GL (Fin 2) ℝ)) ⧸
(↑(CongruenceSubgroup.Gamma0 2) : Subgroup (GL (Fin 2) ℝ)).subgroupOf
(↑(CongruenceSubgroup.Gamma 1))) = 6 := by
rw [card_quotient_eq_three]; norm_num
have hf0 : (f : ℍ → ℂ) = 0 :=
(CuspForm.norm_eq_zero_iff (↑(CongruenceSubgroup.Gamma 1) : Subgroup (GL (Fin 2) ℝ)) f).1
(S6_levelOne_eq_zero' hweight
(CuspForm.norm (↑(CongruenceSubgroup.Gamma 1) : Subgroup (GL (Fin 2) ℝ)) f))
exact DFunLike.coe_injective (hf0.trans CuspForm.coe_zero.symm)
編集はこのタブに残ります。漫画は元の原文の説明なので、行との対応は一時停止しています。FLT全体をこのサイトで検証することはできません。
👩🏻🎨 ミカ · 原文を読むための案内
部分群の指数[SL₂(ℤ):Γ₀(2)]＝3を使い、CuspForm.normで重さ2をレベル1の重さ6へ移します。S6_levelOne_eq_zero′でノルムが消え、norm_eq_zero_iffからf自身も消えます。この結果はFLTの矛盾を使わず、Mathlibから証明されています。
元の原文への注釈・Leanの実行状態ではありませんコマの手がかりや原文の色つきの語句に触れると、対応をたどれます。
この論理を試してみる →出典と検証の範囲
出典：anthropics/fermats-last-theorem（aa2d8b3）。上流では検証済みと報告されていますが、このアプリでは全体を再ビルド・再検証していません。漫画の解説自体は形式的な証明ではありません。
ソースのライセンスと著作者表示まず、この言葉から
知っている言葉は飛ばして大丈夫。初めてなら、言葉を開くか、基礎から順に読んでみよう。
- 関数関数は、入れてよい値のそれぞれに出力を一つ決めます。
- 重さとレベル重さは変換の規則、レベルはどの変換に規則を求めるかを指定します。
- カスプ形式モジュラー形式に、すべての尖点で0へ近づく条件を加えたもの。
- 誰もいない部屋ある重さとレベルの空間では、すべてのカスプ形式が0だと定理で示します。
- 同じ対象についての矛盾同じfについて、f ≠ 0とf = 0の証拠は両立しません。
物語 → 証明三つの入口は部分群の指数。数えることで、重さ2を重さ6へ変える倍率を確かめます。
商の大きさを数えるcard_quotient_eq_three物語 → 証明移した先の譜面台も静かになるのは、重さ6・レベル1での消滅定理がそこで使えるからです。
消えることを示す依存先S6_levelOne_eq_zero'物語 → 証明元の譜面台へ戻るのは、関数としての等しさから形式としての等しさを取り戻すことです。
関数から形式に戻るDFunLike.coe_injective物語の向こうにある考え方
部分群の指数[SL₂(ℤ):Γ₀(2)]＝3を使い、CuspForm.normで重さ2をレベル1の重さ6へ移します。S6_levelOne_eq_zero′でノルムが消え、norm_eq_zero_iffからf自身も消えます。この結果はFLTの矛盾を使わず、Mathlibから証明されています。
重さ6が現れる理由は？
- 重さ2に部分群の指数3を掛けるから。
- 6番目の章だから。
このページで物語と原文を読めます。証明の編集、クイズ、対話式のマップにはJavaScriptを有効にしてください。
練習用のリアルタイム検査
証明の続きを、あなたの手で。
小さな場面、本物の論理の目標。そして、あなたの成功を気にかけるハト。
事件簿を開いています…