ピップ
「正しい布をたくさん見つけた。これでキルトは完成？」
キルト完成宣言物語 → 証明ばらばらの布は入力の部品。パッチングのデータは、接続が合うための条件も指定します。
部品と整合性Algebra.PatchingDatum「なぜ？」から始まる、数学の冒険
小さな「なぜ？」。 大きな冒険。
物語を追い、証明に触れる。気になったら、もうひとつ奥まで。
アカウント不要。APIキー不要。好奇心だけで。
ふたつの入口。お茶の間は、ひとつ。
今日は数学と戦わないまんがから入ります:17章、64個の小石、必須の式はゼロ。Leanの原文は、訪ねてくるまでガラス越しです。
数学へまっすぐ証明マップから始めます:名付けられた定理が数千本。そして時計の逆元からR = Tまで、階段を全部登ります。となりでは物語も語り続け、あなたを正直に保ちます。
ふたりで読むために作りました:数学好きと、数学が苦手なひと。ソファは一台。それぞれが持ち帰ったものは、お茶の間へ運びます。
「まだわからない」から始めよう。
全17章で、ひとつの大きな道筋へ。今日は、小さな発見がひとつあれば十分。
全17章 · Lean元の原文 ↗
ピップの心得：まちがいも手がかり。どの章にも進めて、何度でも考え直せます。
モジュラー性、3–5の切り替え、つながる部品。
証明全体のマップを開く29,511の定理・正確な主張・依存関係
英語や日本語で定理を検索できます。主要な定理には日本語の見出しがあります。文脈全体はGitHubの原文から確かめられます。
この章で見つけたいこと
正しい部品を集めるだけでなく、つなぎ目の整合性も必要だと知ろう。
- Nonempty
- その型に少なくとも一つの要素が存在するという命題。
- Subsingleton
- 任意の二つの要素が等しい、つまり要素が高々一つという性質。
元の原文 ↗ · L3779–3789固定版 aa2d8b3
theorem solution
{𝒪 : Type} [CommRing 𝒪] [IsDomain 𝒪] [IsDiscreteValuationRing 𝒪]
[IsAdicComplete (IsLocalRing.maximalIdeal 𝒪) 𝒪] [Finite (IsLocalRing.ResidueField 𝒪)]
{ℓ r : ℕ} (hℓ : (ℓ : 𝒪) ∈ IsLocalRing.maximalIdeal 𝒪)
{R : Type} [CommRing R] [Algebra 𝒪 R] {M : Type} [AddCommGroup M] [Module R M]
(P : Algebra.PatchingDatum 𝒪 ℓ r R M) :
Nonempty (Algebra.PatchingLevel 𝒪 r R M ⊥) := by
rcases subsingleton_or_nontrivial M with hM | hM
· exact ⟨FrobDictPC.Limit.trivialLevel P⟩
· haveI : Fact ((ℓ : 𝒪) ∈ IsLocalRing.maximalIdeal 𝒪) := ⟨hℓ⟩
exact ⟨FrobDictPC.Limit.patchedLevel P⟩
編集はこのタブに残ります。漫画は元の原文の説明なので、行との対応は一時停止しています。FLT全体をこのサイトで検証することはできません。
👩🏻🎨 ミカ · 原文を読むための案内
目標はNonempty (Algebra.PatchingLevel 𝒪 r R M ⊥)です。rcases subsingleton_or_nontrivial Mで場合分けし、自明な枝ではtrivialLevel Pを包みます。非自明な枝はFact hℓを登録し、patchedLevel Pを包みます。最後の呼び出しに至る構成は、前の数千行にあります。
元の原文への注釈・Leanの実行状態ではありませんコマの手がかりや原文の色つきの語句に触れると、対応をたどれます。
この論理を試してみる →出典と検証の範囲
出典：anthropics/fermats-last-theorem（aa2d8b3）。上流では検証済みと報告されていますが、このアプリでは全体を再ビルド・再検証していません。漫画の解説自体は形式的な証明ではありません。
ソースのライセンスと著作者表示まず、この言葉から
知っている言葉は飛ばして大丈夫。初めてなら、言葉を開くか、基礎から順に読んでみよう。
- 足し算とかけ算の仕組み足し算とかけ算の規則をそろえると、別の数の世界を同じ言葉で比べられます。
- 変形環と普遍性条件に合う持ち上げを、一つの代数的な対象からの写像で整理します。
- ヘッケ環カスプ形式への特別な操作と、それが持つ算術の情報を集めます。
- R = T——二つの工房をつなぐ等式持ち上げから作る環と、ヘッケ作用素から作る環を、一つの全射の写像で結びます。
- パッチング部品だけでなく接続の条件もそろえ、一つの対象を作ります。
ミカ
「接続する端も合わないとね。入力に、どうつながるべきかを指定しておくんだ。」
つなぎ目が大事物語 → 証明布の端をそろえて、一つの整合した対象を目指します。Nonemptyは、要求を満たす実物を一つ示すという目標です。
目標は存在を示すことNonempty (Algebra.PatchingLevelピップ
「ほとんど空のキルト？ 練習の少ない役が、ついに来た。」
静かな特別扱い物語 → 証明空の布枠は、要素が高々一つの特別な場合のたとえ。その場合はtrivialLevelという構成を使えます。
特別な場合の構成FrobDictPC.Limit.trivialLevelミカ
「それ以外の場合は、ここまでに作った構成でつながる対象を用意するよ。難しい仕事はそこにあるんだ。」
ちゃんとつながった物語 → 証明縫い合わされた橋は、残る場合にpatchedLevelが与える実物。部品の山や適当なのりだけでは足りません。
つなぎ合わせた橋FrobDictPC.Limit.patchedLevel物語の向こうにある考え方
目標はNonempty (Algebra.PatchingLevel 𝒪 r R M ⊥)です。rcases subsingleton_or_nontrivial Mで場合分けし、自明な枝ではtrivialLevel Pを包みます。非自明な枝はFact hℓを登録し、patchedLevel Pを包みます。最後の呼び出しに至る構成は、前の数千行にあります。
非自明な枝を閉じるものは？
- patchedLevel Pで構成した要素。
- すべての曲線についての有限探索。
このページで物語と原文を読めます。証明の編集、クイズ、対話式のマップにはJavaScriptを有効にしてください。
練習用のリアルタイム検査
証明の続きを、あなたの手で。
小さな場面、本物の論理の目標。そして、あなたの成功を気にかけるハト。
事件簿を開いています…