物語 → 証明黄色い助っ人が役立つのは、3を法とする表現が既約だから。見た目が似た代役だけでは務まりません。
3に向いた助っ人W'.ModRepIsIrreducible 3「なぜ？」から始まる、数学の冒険
小さな「なぜ？」。 大きな冒険。
物語を追い、証明に触れる。気になったら、もうひとつ奥まで。
アカウント不要。APIキー不要。好奇心だけで。
ふたつの入口。お茶の間は、ひとつ。
今日は数学と戦わないまんがから入ります:17章、64個の小石、必須の式はゼロ。Leanの原文は、訪ねてくるまでガラス越しです。
数学へまっすぐ証明マップから始めます:名付けられた定理が数千本。そして時計の逆元からR = Tまで、階段を全部登ります。となりでは物語も語り続け、あなたを正直に保ちます。
ふたりで読むために作りました:数学好きと、数学が苦手なひと。ソファは一台。それぞれが持ち帰ったものは、お茶の間へ運びます。
「まだわからない」から始めよう。
全17章で、ひとつの大きな道筋へ。今日は、小さな発見がひとつあれば十分。
全17章 · Lean元の原文 ↗
ピップの心得：まちがいも手がかり。どの章にも進めて、何度でも考え直せます。
モジュラー性、3–5の切り替え、つながる部品。
証明全体のマップを開く29,511の定理・正確な主張・依存関係
英語や日本語で定理を検索できます。主要な定理には日本語の見出しがあります。文脈全体はGitHubの原文から確かめられます。
この章で見つけたいこと
直接は進めない問題を、条件のそろった助っ人で解く方法を知ろう。
- 存在の証拠
- 対象そのものと、要求された性質の証明。
- exact_mod_cast
- 整合する数の型変換を正規化して目標を閉じるタクティク。
元の原文 ↗ · L11–15固定版 aa2d8b3
theorem solution (W : WeierstrassCurve ℤ) (hΔ : W.Δ ≠ 0) (hW : W.IsSemistableModel) (h5 : W.ModRepIsIrreducible 5) : ∃ W' : WeierstrassCurve ℤ, W'.Δ ≠ 0 ∧ W'.IsSemistableModel ∧ W'.ModRepIsIrreducible 3 ∧ ∀ ℓ : ℕ, ℓ.Prime → W.IsGoodPrimeFor ℓ → W'.IsGoodPrimeFor ℓ → ℓ ≠ 5 → (5 : ℤ) ∣ (W'.apOfModel ℓ - W.apOfModel ℓ) := by
obtain ⟨W', hΔ', hW', h3', hφ⟩ := threeFiveAuxiliaryCurveExists W hΔ hW h5
refine ⟨W', hΔ', hW', h3', fun ℓ hℓ hℓW hℓW' hℓ5 => ?_⟩
exact_mod_cast
apOfModel_congr_of_torsionGaloisCongruent 5 Nat.prime_five W W' hΔ hΔ' hφ ℓ hℓ hℓW hℓW' hℓ5
編集はこのタブに残ります。漫画は元の原文の説明なので、行との対応は一時停止しています。FLT全体をこのサイトで検証することはできません。
👩🏻🎨 ミカ · 原文を読むための案内
threeFiveAuxiliaryCurveExistsからW′、hΔ′、hW′、h3′、hφを得ます。refineでこれらを返し、係数の合同だけを目標に残します。apOfModel_congr_of_torsionGaloisCongruentを適用し、exact_mod_castで数の型変換を合わせます。
元の原文への注釈・Leanの実行状態ではありませんコマの手がかりや原文の色つきの語句に触れると、対応をたどれます。
この論理を試してみる →出典と検証の範囲
出典：anthropics/fermats-last-theorem（aa2d8b3）。上流では検証済みと報告されていますが、このアプリでは全体を再ビルド・再検証していません。漫画の解説自体は形式的な証明ではありません。
ソースのライセンスと著作者表示まず、この言葉から
知っている言葉は飛ばして大丈夫。初めてなら、言葉を開くか、基礎から順に読んでみよう。
- 形式と表現をつなぐ曲線のデータと形式のデータが、余りの世界の中で一致することを一つの主張にまとめます。
- 既約性すべての対称性で保たれる部分空間は、0だけか全体だけ。
- 半安定性素数ごとに余りの世界へ移したときの曲線のふるまいを制限します。
- 残余モジュラー性余りの世界へ移した算術データが、形式の係数と一致すること。
- 持ち上げ追加条件のある定理で、余りの情報から元の豊かな情報へ進みます。
物語 → 証明助っ人の証明書は、条件つきの存在定理が用意します。ミカが都合のよい助っ人を勝手に仮定するわけではありません。
存在定理で助っ人を得るthreeFiveAuxiliaryCurveExists物語 → 証明帽子ではなくカードを比べるのが算術の整合性の役。情報を移すには、対象の素数ごとの条件も必要です。
素数ごとの条件を受け取るfun ℓ hℓ hℓW hℓW' hℓ5物語 → 証明カードを元の装置へ戻すのは、共通の良い素数での係数の合同を、元のモデルへ持ち帰ることです。
合同という手がかりを移すapOfModel_congr_of_torsionGaloisCongruent物語の向こうにある考え方
threeFiveAuxiliaryCurveExistsからW′、hΔ′、hW′、h3′、hφを得ます。refineでこれらを返し、係数の合同だけを目標に残します。apOfModel_congr_of_torsionGaloisCongruentを適用し、exact_mod_castで数の型変換を合わせます。
5を法とする合同を表す式はどちら？
- 5∣(aℓ(W′)−aℓ(W))
- すべての素数でaℓ(W′)＝5
このページで物語と原文を読めます。証明の編集、クイズ、対話式のマップにはJavaScriptを有効にしてください。
練習用のリアルタイム検査
証明の続きを、あなたの手で。
小さな場面、本物の論理の目標。そして、あなたの成功を気にかけるハト。
事件簿を開いています…