ピップ
「不可能なケーキの注文、お願いします:三つの高さがa ^ n + b ^ n = c ^ nを満たす塔です。」
二乗ならご注文どおり物語 → 証明ケーキの注文は、等式を満たす数を探すこと。二乗での成功は、この定理の指数の範囲外です。
成立しない等式a ^ n + b ^ n ≠ c ^ n「なぜ？」から始まる、数学の冒険
小さな「なぜ？」。 大きな冒険。
物語を追い、証明に触れる。気になったら、もうひとつ奥まで。
アカウント不要。APIキー不要。好奇心だけで。
ふたつの入口。お茶の間は、ひとつ。
今日は数学と戦わないまんがから入ります:17章、64個の小石、必須の式はゼロ。Leanの原文は、訪ねてくるまでガラス越しです。
数学へまっすぐ証明マップから始めます:名付けられた定理が数千本。そして時計の逆元からR = Tまで、階段を全部登ります。となりでは物語も語り続け、あなたを正直に保ちます。
ふたりで読むために作りました:数学好きと、数学が苦手なひと。ソファは一台。それぞれが持ち帰ったものは、お茶の間へ運びます。
「まだわからない」から始めよう。
全17章で、ひとつの大きな道筋へ。今日は、小さな発見がひとつあれば十分。
全17章 · Lean元の原文 ↗
ピップの心得：まちがいも手がかり。どの章にも進めて、何度でも考え直せます。
累乗、問題の還元、あやしい小包。
証明全体のマップを開く29,511の定理・正確な主張・依存関係
英語や日本語で定理を検索できます。主要な定理には日本語の見出しがあります。文脈全体はGitHubの原文から確かめられます。
この章で見つけたいこと
フェルマーの最終定理が「何を言っているか」をつかもう。
- ha.ne'
- 0<aという証拠からa≠0という証拠を得る。
- 定理の適用
- 仮定の証拠を受け取り、結論の証拠を返すものとして定理を使う。
元の原文 ↗ · L129–130固定版 aa2d8b3
theorem solution (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n :=
FLT.fermatLastTheorem n hn a b c ha.ne' hb.ne' hc.ne'
編集はこのタブに残ります。漫画は元の原文の説明なので、行との対応は一時停止しています。FLT全体をこのサイトで検証することはできません。
👩🏻🎨 ミカ · 原文を読むための案内
この短い証明はFLT.fermatLastTheoremを呼び出します。ha.ne'、hb.ne'、hc.ne'は、正であるという証拠を非零の証拠に変換します。長い本体は、ここで使う定理とその依存先にあります。
元の原文への注釈・Leanの実行状態ではありませんコマの手がかりや原文の色つきの語句に触れると、対応をたどれます。
この論理を試してみる →出典と検証の範囲
出典：anthropics/fermats-last-theorem（aa2d8b3）。上流では検証済みと報告されていますが、このアプリでは全体を再ビルド・再検証していません。漫画の解説自体は形式的な証明ではありません。
ソースのライセンスと著作者表示まず、この言葉から
知っている言葉は飛ばして大丈夫。初めてなら、言葉を開くか、基礎から順に読んでみよう。
- 累乗と正の整数累乗は同じ数を繰り返しかけること。正の整数は1から。
- 偶数・奇数と場合分け数を偶数と奇数に分けるのは、この証明そのものが使う最初の場合分けです。
- 仮の反例とフライ小包ないはずの解を仮に置き、数と条件の証拠をまとめます。
ミカ
「ちゅうい。二乗なら本当に成立します——2は範囲外。この規則は3以上でしかかみつきません。」
ほんの少し変えたら物語 → 証明立方体のケーキへの変更が、指数の条件を表します。三つの累乗で同じnを使い、nは3以上です。
指数は3以上hn : 3 ≤ nピップ
「空のお皿禁止、ゼロの塔禁止。ミカが入口で全員点検:高さは正の数だけ。」
空のお皿は禁止物語 → 証明ピップの空のお皿は0。ミカに止められるのは、正の数という条件があるから。bとcにも同じ条件があります。
空のお皿は禁止ha : 0 < aミカ
「封筒は、条件に合うすべての注文を一度に束ねます。署名ひとつで、事件全体が閉じます。」
とても大きな約束物語 → 証明封筒に入れた事件は、条件に合うすべての注文についての約束。最後の行で、その約束を支える定理を使います。
約束を支える定理FLT.fermatLastTheorem物語の向こうにある考え方
この短い証明はFLT.fermatLastTheoremを呼び出します。ha.ne'、hb.ne'、hc.ne'は、正であるという証拠を非零の証拠に変換します。長い本体は、ここで使う定理とその依存先にあります。
haではなくha.ne'を渡す理由は？
- 正の整数を無作為に選ぶため。
- 呼び出す定理が非零の証拠を求めるため。
このページで物語と原文を読めます。証明の編集、クイズ、対話式のマップにはJavaScriptを有効にしてください。
練習用のリアルタイム検査
証明の続きを、あなたの手で。
小さな場面、本物の論理の目標。そして、あなたの成功を気にかけるハト。
事件簿を開いています…