物語 → 証明かばんはモジュラー性の入場証を持って到着します。レベルを下げる前に、その証拠が必要です。
モジュラー性の証拠hmod : P.freyCurve.IsModular「なぜ？」から始まる、数学の冒険
小さな「なぜ？」。 大きな冒険。
物語を追い、証明に触れる。気になったら、もうひとつ奥まで。
アカウント不要。APIキー不要。好奇心だけで。
ふたつの入口。お茶の間は、ひとつ。
今日は数学と戦わないまんがから入ります:17章、64個の小石、必須の式はゼロ。Leanの原文は、訪ねてくるまでガラス越しです。
数学へまっすぐ証明マップから始めます:名付けられた定理が数千本。そして時計の逆元からR = Tまで、階段を全部登ります。となりでは物語も語り続け、あなたを正直に保ちます。
ふたりで読むために作りました:数学好きと、数学が苦手なひと。ソファは一台。それぞれが持ち帰ったものは、お茶の間へ運びます。
「まだわからない」から始めよう。
全17章で、ひとつの大きな道筋へ。今日は、小さな発見がひとつあれば十分。
全17章 · Lean元の原文 ↗
ピップの心得：まちがいも手がかり。どの章にも進めて、何度でも考え直せます。
レベルを下げ、空の部屋を開け、事件を解決する。
証明全体のマップを開く29,511の定理・正確な主張・依存関係
英語や日本語で定理を検索できます。主要な定理には日本語の見出しがあります。文脈全体はGitHubの原文から確かめられます。
この章で見つけたいこと
二つの枝の成果から、レベル2の非零カスプ形式を導く道筋を知ろう。
- 存在の組
- 対象と、その対象に必要な性質の証拠の組。
元の原文 ↗ · L129–134固定版 aa2d8b3
set_option linter.unusedVariables false in
theorem solution (P : FreyPackage) (hmod : P.freyCurve.IsModular)
(hirr : GaloisRepIsIrreducible (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p) :
∃ f : CuspForm (CongruenceSubgroup.Gamma0 2) 2, f ≠ 0 := by
obtain ⟨N, hcond, hmodN⟩ := P.modularRepOfConductorLevel
exact P.level_lowering_to_two_of_conductorLevel hirr hcond hmodN
編集はこのタブに残ります。漫画は元の原文の説明なので、行との対応は一時停止しています。FLT全体をこのサイトで検証することはできません。
👩🏻🎨 ミカ · 原文を読むための案内
P、hmod、hirrから、∃ f : CuspForm (Gamma0 2) 2, f≠0を結論します。obtainでN、hcond、hmodNを取得し、exactでhirrとともにレベル下げの定理へ渡します。unusedVariablesの設定は、hmodを使わないこの実装に対応しています。
元の原文への注釈・Leanの実行状態ではありませんコマの手がかりや原文の色つきの語句に触れると、対応をたどれます。
この論理を試してみる →出典と検証の範囲
出典：anthropics/fermats-last-theorem（aa2d8b3）。上流では検証済みと報告されていますが、このアプリでは全体を再ビルド・再検証していません。漫画の解説自体は形式的な証明ではありません。
ソースのライセンスと著作者表示まず、この言葉から
知っている言葉は飛ばして大丈夫。初めてなら、言葉を開くか、基礎から順に読んでみよう。
- 曲線のモジュラー性曲線の算術データと係数が一致する、条件つきの形式を見つけること。
- 既約性すべての対称性で保たれる部分空間は、0だけか全体だけ。
- 導手とレベル下げ注意すべき素数を記録し、証明済みの条件でレベルの素因子を制限します。
- カスプ形式モジュラー形式に、すべての尖点で0へ近づく条件を加えたもの。
物語 → 証明目的の部屋は重さ2・レベル2のカスプ形式の空間。後の矛盾のため、来客は0ではない必要があります。
レベル2・重さ2へCuspForm (CongruenceSubgroup.Gamma0 2) 2物語 → 証明入場証を受け取るのは、導手レベルの情報と条件を集めること。荷物を持つ係の冗談では、その証拠は得られません。
導手の情報を集めるP.modularRepOfConductorLevel物語 → 証明確認した荷札を外すのは、依存先の深いレベル下げの定理の役。必要な非零の形式を残して進みます。
レベル下げの定理を使うP.level_lowering_to_two_of_conductorLevel物語の向こうにある考え方
P、hmod、hirrから、∃ f : CuspForm (Gamma0 2) 2, f≠0を結論します。obtainでN、hcond、hmodNを取得し、exactでhirrとともにレベル下げの定理へ渡します。unusedVariablesの設定は、hmodを使わないこの実装に対応しています。
この本体でhmodはどこに使われている？
- 使われていない。導手レベルの依存先が必要な情報を再び得る。
- hirrという名前の中に使われている。
このページで物語と原文を読めます。証明の編集、クイズ、対話式のマップにはJavaScriptを有効にしてください。
練習用のリアルタイム検査
証明の続きを、あなたの手で。
小さな場面、本物の論理の目標。そして、あなたの成功を気にかけるハト。
事件簿を開いています…