ピップ
「3音なら吹ける。小さな曲から、コンサート全体へどう進むの？」
小さなオーディション物語 → 証明ピップの3音の試演は残余モジュラー性への入口。レベルが正という仮定も、別に用意する必要があります。
正のレベル0 < M「なぜ？」から始まる、数学の冒険
小さな「なぜ？」。 大きな冒険。
物語を追い、証明に触れる。気になったら、もうひとつ奥まで。
アカウント不要。APIキー不要。好奇心だけで。
ふたつの入口。お茶の間は、ひとつ。
今日は数学と戦わないまんがから入ります:17章、64個の小石、必須の式はゼロ。Leanの原文は、訪ねてくるまでガラス越しです。
数学へまっすぐ証明マップから始めます:名付けられた定理が数千本。そして時計の逆元からR = Tまで、階段を全部登ります。となりでは物語も語り続け、あなたを正直に保ちます。
ふたりで読むために作りました:数学好きと、数学が苦手なひと。ソファは一台。それぞれが持ち帰ったものは、お茶の間へ運びます。
「まだわからない」から始めよう。
全17章で、ひとつの大きな道筋へ。今日は、小さな発見がひとつあれば十分。
全17章 · 物語元の原文 ↗
ピップの心得：まちがいも手がかり。どの章にも進めて、何度でも考え直せます。
モジュラー性、3–5の切り替え、つながる部品。
証明全体のマップを開く29,511の定理・正確な主張・依存関係
英語や日本語で定理を検索できます。主要な定理には日本語の見出しがあります。文脈全体はGitHubの原文から確かめられます。
この章で見つけたいこと
3を法とするモジュラーな情報が、証明の大切な出発点になることを知ろう。
- 3を法とする
- 3で割った余りに注目して情報を比べること。
- 出発点
- それ自体は弱い結果でも、次の定理を使う入口になるもの。
元の原文 ↗ · L67–84固定版 aa2d8b3
theorem solution
(W : WeierstrassCurve ℤ) (hΔ : W.Δ ≠ 0) (hW : W.IsSemistableModel)
(h3 : W.ModRepIsIrreducible 3) :
∃ M : ℕ, 0 < M ∧ W.IsResiduallyModularOfLevel 3 M ∧
(∀ q : ℕ, q.Prime → q ≠ 3 → ¬ q ^ 3 ∣ M) ∧
(3 ^ 2 ∣ M →
∀ A : ValuationSubring (AlgebraicClosure ℚ), A.LiesOverPrime 3 →
∀ x : Submodule.torsionBy ℤ
((W.map (Int.castRingHom ℚ))⁄(AlgebraicClosure ℚ)).Point (3 : ℕ),
(∀ σ ∈ A.inertiaSubgroupIn ℚ, σ • x = x) → x = 0) := by
obtain ⟨N, hNZ, a, hbasis, heig, hreal, hcube, htr, hns⟩ :=
haveI : NeZero N := hNZ
refine ⟨N, Nat.pos_of_ne_zero hNZ.out, ?_, hcube, hns⟩
obtain ⟨f, hf, 𝔪', h𝔪max, h𝔪3, hcong⟩ :=
hbasis heig hreal
refine ⟨f, 𝔪', hf, h𝔪max, h𝔪3, ?_⟩
編集はこのタブに残ります。漫画は元の原文の説明なので、行との対応は一時停止しています。FLT全体をこのサイトで検証することはできません。
👩🏻🎨 ミカ · 原文を読むための案内
まず、余りの情報を持つ形式を見つけます。一つ目の定理は、出発点になる重さ1の形式を用意します。次の定理で必要な一致を保ったまま、重さ2の形式へ進みます。それが持ち上げに渡す入力になります。定理の名前の前に、関数・係数・重さの意味から読もう。
元の原文への注釈・Leanの実行状態ではありませんコマの手がかりや原文の色つきの語句に触れると、対応をたどれます。
この論理を試してみる →出典と検証の範囲
出典：anthropics/fermats-last-theorem（aa2d8b3）。上流では検証済みと報告されていますが、このアプリでは全体を再ビルド・再検証していません。漫画の解説自体は形式的な証明ではありません。
ソースのライセンスと著作者表示まず、この言葉から
知っている言葉は飛ばして大丈夫。初めてなら、言葉を開くか、基礎から順に読んでみよう。
- 余りで比べる・合同数が違っていても、割った余りが同じなら合同です。
- 時計の算術余りの集合を決め、その中だけで計算する世界を作ります。
- 行列という変換二行二列の数の表が変換を表し、行列どうしの掛け算もできます。
- 行列の合同部分群レベルは、保つ行列の変換と、余りの世界で0に送られる変換を指定します。
- モジュラー形式複素数を返し、変換と滑らかさについて厳密な規則を持つ関数。
- 係数という数のデータ関数を展開して、数の列として読むときの一つひとつの数。
- 重さとレベル重さは変換の規則、レベルはどの変換に規則を求めるかを指定します。
- カスプ形式モジュラー形式に、すべての尖点で0へ近づく条件を加えたもの。
- 正規化された固有形式係数の列に追加の算術規則があり、最初の係数を1にそろえます。
- 残余モジュラー性余りの世界へ移した算術データが、形式の係数と一致すること。
- 持ち上げ追加条件のある定理で、余りの情報から元の豊かな情報へ進みます。
物語 → 証明旋律には条件の用紙が付きます。特にレベルがqの三乗で割り切れないという条件を残します。
導手の条件を残す¬ q ^ 3 ∣ M物語 → 証明小さな楽器は出発点の重さ1の形式。ピップの試演ではなく、名前つきの定理からそれを得ます。
最初の旋律の出典FLT.No2BridgeWiring.weightOneNewformExists_levelAtThree_not_cube_dvd物語 → 証明大きな楽器へ色玉を移すのは、算術の情報を保ちながら合同な重さ2の固有形式を得ることです。
重さ2へ移すFLT.AbstractIntegralStructure.exists_weight_two_eigenform_congruent_of_isLatticeRealized物語の向こうにある考え方
まず、余りの情報を持つ形式を見つけます。一つ目の定理は、出発点になる重さ1の形式を用意します。次の定理で必要な一致を保ったまま、重さ2の形式へ進みます。それが持ち上げに渡す入力になります。定理の名前の前に、関数・係数・重さの意味から読もう。
小さく還元した指紋が役立つのはなぜ？
- それだけで何でも証明できるから。
- 条件つきの持ち上げ定理を使う出発点になるから。
このページで物語と原文を読めます。証明の編集、クイズ、対話式のマップにはJavaScriptを有効にしてください。
練習用のリアルタイム検査
証明の続きを、あなたの手で。
小さな場面、本物の論理の目標。そして、あなたの成功を気にかけるハト。
事件簿を開いています…