ピップ
「事件ファイルが天井まで積まれています。一枚ずつ確認していたら、紙の寿命のほうが先です。」
無限の事務作業物語 → 証明ファイルの山は無限にある指数。終わらないチェックリストでは、すべての場合の結論に届きません。
すべての指数FermatLastTheorem「なぜ？」から始まる、数学の冒険
小さな「なぜ？」。 大きな冒険。
物語を追い、証明に触れる。気になったら、もうひとつ奥まで。
アカウント不要。APIキー不要。好奇心だけで。
ふたつの入口。お茶の間は、ひとつ。
今日は数学と戦わないまんがから入ります:17章、64個の小石、必須の式はゼロ。Leanの原文は、訪ねてくるまでガラス越しです。
数学へまっすぐ証明マップから始めます:名付けられた定理が数千本。そして時計の逆元からR = Tまで、階段を全部登ります。となりでは物語も語り続け、あなたを正直に保ちます。
ふたりで読むために作りました:数学好きと、数学が苦手なひと。ソファは一台。それぞれが持ち帰ったものは、お茶の間へ運びます。
「まだわからない」から始めよう。
全17章で、ひとつの大きな道筋へ。今日は、小さな発見がひとつあれば十分。
全17章 · 物語元の原文 ↗
ピップの心得：まちがいも手がかり。どの章にも進めて、何度でも考え直せます。
累乗、問題の還元、あやしい小包。
証明全体のマップを開く29,511の定理・正確な主張・依存関係
英語や日本語で定理を検索できます。主要な定理には日本語の見出しがあります。文脈全体はGitHubの原文から確かめられます。
この章で見つけたいこと
無限にある指数を、一つずつ調べずに扱う方法を知ろう。
- 素数
- 1より大きく、正の約数が1と自分自身だけの整数。
元の原文 ↗ · L130–139固定版 aa2d8b3
theorem solution : FermatLastTheorem := by
apply FermatLastTheorem.of_odd_primes
intro p pp p_odd
by_cases hp5 : 5 ≤ p
· exact FreyPackage.fermatLastTheoremFor_of_five_le p pp hp5
· have hp2 := pp.two_le
interval_cases p
· exact absurd p_odd (by decide)
· exact fermatLastTheoremThree
· exact absurd pp (by decide)
編集はこのタブに残ります。漫画は元の原文の説明なので、行との対応は一時停止しています。FLT全体をこのサイトで検証することはできません。
👩🏻🎨 ミカ · 原文を読むための案内
指数の山は無限に続き、フォルダを一枚ずつ確認していては終わりません。そこで証明は地図を折ります:指数4と奇素数が落ちれば、ほかはすべてその蓋の下に収まります。指数3の引き出しはすでに閉まっていて、大きな素数のフォルダはフライ小包の班と一緒に旅立ちます。
元の原文への注釈・Leanの実行状態ではありませんコマの手がかりや原文の色つきの語句に触れると、対応をたどれます。
この論理を試してみる →出典と検証の範囲
出典：anthropics/fermats-last-theorem（aa2d8b3）。上流では検証済みと報告されていますが、このアプリでは全体を再ビルド・再検証していません。漫画の解説自体は形式的な証明ではありません。
ソースのライセンスと著作者表示まず、この言葉から
知っている言葉は飛ばして大丈夫。初めてなら、言葉を開くか、基礎から順に読んでみよう。
この章を基礎から順に説明して →物語 → 証明地図を折りたたむのは問題の還元。指数4と奇素数の場合を押さえると、元の主張をすべて扱えます。
奇素数にしぼるFermatLastTheorem.of_odd_primes物語 → 証明閉じた引き出しは解決済みの指数3。場合分けによって、5以上の素数と切り分けます。
小さな場合を分けるby_cases hp5 : 5 ≤ p物語 → 証明小さなかばんには、残った5以上の素数の場合を入れます。フライ小包の定理へ進んでも、場合を取りこぼしません。
大きな素数の証明へFreyPackage.fermatLastTheoremFor_of_five_le物語の向こうにある考え方
指数の山は無限に続き、フォルダを一枚ずつ確認していては終わりません。そこで証明は地図を折ります:指数4と奇素数が落ちれば、ほかはすべてその蓋の下に収まります。指数3の引き出しはすでに閉まっていて、大きな素数のフォルダはフライ小包の班と一緒に旅立ちます。
a⁶＋b⁶＝c⁶を、指数3の式に直すと？
- (a²)³＋(b²)³＝(c²)³
- (a＋2)³＋(b＋2)³＝(c＋2)³
このページで物語と原文を読めます。証明の編集、クイズ、対話式のマップにはJavaScriptを有効にしてください。
練習用のリアルタイム検査
証明の続きを、あなたの手で。
小さな場面、本物の論理の目標。そして、あなたの成功を気にかけるハト。
事件簿を開いています…