物語 → 証明装置の指紋は算術のデータ。相方の形式の係数が、指定された素数でそれと一致する必要があります。
算術の楽譜を合わせるModularFormClass.qCoeff f p「なぜ？」から始まる、数学の冒険
小さな「なぜ？」。 大きな冒険。
物語を追い、証明に触れる。気になったら、もうひとつ奥まで。
アカウント不要。APIキー不要。好奇心だけで。
ふたつの入口。お茶の間は、ひとつ。
今日は数学と戦わないまんがから入ります:17章、64個の小石、必須の式はゼロ。Leanの原文は、訪ねてくるまでガラス越しです。
数学へまっすぐ証明マップから始めます:名付けられた定理が数千本。そして時計の逆元からR = Tまで、階段を全部登ります。となりでは物語も語り続け、あなたを正直に保ちます。
ふたりで読むために作りました:数学好きと、数学が苦手なひと。ソファは一台。それぞれが持ち帰ったものは、お茶の間へ運びます。
「まだわからない」から始めよう。
全17章で、ひとつの大きな道筋へ。今日は、小さな発見がひとつあれば十分。
全17章 · Lean元の原文 ↗
ピップの心得：まちがいも手がかり。どの章にも進めて、何度でも考え直せます。
曲線の算術を、勝手に切り分けられない理由。
証明全体のマップを開く29,511の定理・正確な主張・依存関係
英語や日本語で定理を検索できます。主要な定理には日本語の見出しがあります。文脈全体はGitHubの原文から確かめられます。
この章で見つけたいこと
「モジュラーである」とは、曲線と形式の算術が対応することだと知ろう。
- ∃
- 対象と、それが条件を満たす証明の存在を表す。
- 定義と定理
- 性質の意味を決めることと、その性質が成り立つと証明することは別。
元の原文 ↗ · L93–102固定版 aa2d8b3
def IsModularModelOfLevel (W : WeierstrassCurve ℤ) (N : ℕ) : Prop :=
∃ f : CuspForm (CongruenceSubgroup.Gamma0 N) 2, f.IsNormalizedEigenform ∧
∀ p : ℕ, p.Prime → W.IsGoodPrimeFor p → ¬ p ∣ N →
ModularFormClass.qCoeff f p = (W.apOfModel p : ℂ)
def IsModularModel (W : WeierstrassCurve ℤ) : Prop :=
∃ N : ℕ, 0 < N ∧ W.IsModularModelOfLevel N
def IsModular (E : WeierstrassCurve ℚ) : Prop :=
∃ W : WeierstrassCurve ℤ, W.IsIntegralModelOf E ∧ W.IsModularModel
編集はこのタブに残ります。漫画は元の原文の説明なので、行との対応は一時停止しています。FLT全体をこのサイトで検証することはできません。
👩🏻🎨 ミカ · 原文を読むための案内
定義を読むときは∃が要求する対象と、∀以下の条件を分けて追います。固定したNでの性質から、正のNの存在、整数モデルの存在へと定義が重なっています。この抜粋は定義であり、フライ曲線のモジュラー性を証明する本体ではありません。
元の原文への注釈・Leanの実行状態ではありませんコマの手がかりや原文の色つきの語句に触れると、対応をたどれます。
この論理を試してみる →出典と検証の範囲
出典：anthropics/fermats-last-theorem（aa2d8b3）。上流では検証済みと報告されていますが、このアプリでは全体を再ビルド・再検証していません。漫画の解説自体は形式的な証明ではありません。
ソースのライセンスと著作者表示まず、この言葉から
知っている言葉は飛ばして大丈夫。初めてなら、言葉を開くか、基礎から順に読んでみよう。
- 行列という変換二行二列の数の表が変換を表し、行列どうしの掛け算もできます。
- 行列の合同部分群レベルは、保つ行列の変換と、余りの世界で0に送られる変換を指定します。
- スラッシュ作用——重さの正確な規則変換の法則は、束ねた一つの等式です:許されたγすべてに対して f ∣[k] γ = f。
- モジュラー形式複素数を返し、変換と滑らかさについて厳密な規則を持つ関数。
- 係数という数のデータ関数を展開して、数の列として読むときの一つひとつの数。
- 重さとレベル重さは変換の規則、レベルはどの変換に規則を求めるかを指定します。
- カスプ形式モジュラー形式に、すべての尖点で0へ近づく条件を加えたもの。
- 正規化された固有形式係数の列に追加の算術規則があり、最初の係数を1にそろえます。
- 曲線のモジュラー性曲線の算術データと係数が一致する、条件つきの形式を見つけること。
物語 → 証明奏者は条件を備えたモジュラー形式。気持ちよい曲なら何でもよいのではなく、正規化された固有形式を求めます。
条件つきの固有形式f.IsNormalizedEigenformピップ
「二つの数が本当に一致するの？ リハーサルの予算はビスケット一枚です。」
同じ指紋物語 → 証明小さな橋は、ある正のレベルNでの対応。存在を求める条件であり、見た目から作れるという意味ではありません。
レベルは正0 < N物語 → 証明二重奏の指揮は、曲線とその整モデルを結ぶ案内。実際に相方があることは、別のモジュラー性の定理が示します。
二つの記述を結ぶW.IsIntegralModelOf E物語の向こうにある考え方
定義を読むときは∃が要求する対象と、∀以下の条件を分けて追います。固定したNでの性質から、正のNの存在、整数モデルの存在へと定義が重なっています。この抜粋は定義であり、フライ曲線のモジュラー性を証明する本体ではありません。
この抜粋は何をしている？
- モジュラー性という性質の意味を定義している。
- すべての楕円曲線のモジュラー性を証明している。
このページで物語と原文を読めます。証明の編集、クイズ、対話式のマップにはJavaScriptを有効にしてください。
練習用のリアルタイム検査
証明の続きを、あなたの手で。
小さな場面、本物の論理の目標。そして、あなたの成功を気にかけるハト。
事件簿を開いています…