ピップ
「裁判官、こちらが書類です:読み込んだ定理と、依存先の全リスト。数学を書いたわけではありません——運送しただけです。」
最後の窓口物語 → 証明フクロウへ渡す本は、読み込んだ定理とその依存先。この短い確認用ファイルが証明全体ではありません。
実際の定理を読み込むimport Theorems.Thm_fermat_last_theorem「なぜ？」から始まる、数学の冒険
小さな「なぜ？」。 大きな冒険。
物語を追い、証明に触れる。気になったら、もうひとつ奥まで。
アカウント不要。APIキー不要。好奇心だけで。
ふたつの入口。お茶の間は、ひとつ。
今日は数学と戦わないまんがから入ります:17章、64個の小石、必須の式はゼロ。Leanの原文は、訪ねてくるまでガラス越しです。
数学へまっすぐ証明マップから始めます:名付けられた定理が数千本。そして時計の逆元からR = Tまで、階段を全部登ります。となりでは物語も語り続け、あなたを正直に保ちます。
ふたりで読むために作りました:数学好きと、数学が苦手なひと。ソファは一台。それぞれが持ち帰ったものは、お茶の間へ運びます。
「まだわからない」から始めよう。
全17章で、ひとつの大きな道筋へ。今日は、小さな発見がひとつあれば十分。
全17章 · Lean元の原文 ↗
ピップの心得：まちがいも手がかり。どの章にも進めて、何度でも考え直せます。
レベルを下げ、空の部屋を開け、事件を解決する。
証明全体のマップを開く29,511の定理・正確な主張・依存関係
英語や日本語で定理を検索できます。主要な定理には日本語の見出しがあります。文脈全体はGitHubの原文から確かめられます。
この章で見つけたいこと
物語の理解、原文の確認、形式的な検証を区別しよう。
- #guard_msgs
- 処理時に出た診断が、指定された期待する内容と一致するか検査する。
- カーネルとこの読書アプリ
- Leanは証明項を検査。このアプリは原文のハッシュや行対応を保って解説する。
元の原文 ↗ · L1–8固定版 aa2d8b3
import Theorems.Thm_fermat_last_theorem
/-- info: 'fermat_last_theorem' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms fermat_last_theorem
theorem flt_pinned (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n := fermat_last_theorem n hn a b c ha hb hc
theorem flt_mathlib : FermatLastTheorem := fun n hn a b c ha hb hc => fermat_last_theorem n hn a b c (Nat.pos_of_ne_zero ha) (Nat.pos_of_ne_zero hb) (Nat.pos_of_ne_zero hc)
#print axioms flt_mathlib
編集はこのタブに残ります。漫画は元の原文の説明なので、行との対応は一時停止しています。FLT全体をこのサイトで検証することはできません。
👩🏻🎨 ミカ · 原文を読むための案内
#guard_msgsが#print axioms fermat_last_theoremの診断を検査します。flt_pinnedは明示的な型の主張を、flt_mathlibはMathlibのFermatLastTheoremを実現します。原文のスナップショットはカーネル検査の結果ではないので、このアプリではFLTをローカル検証済みとは表示しません。
元の原文への注釈・Leanの実行状態ではありませんコマの手がかりや原文の色つきの語句に触れると、対応をたどれます。
この論理を試してみる →出典と検証の範囲
出典：anthropics/fermats-last-theorem（aa2d8b3）。上流では検証済みと報告されていますが、このアプリでは全体を再ビルド・再検証していません。漫画の解説自体は形式的な証明ではありません。
ソースのライセンスと著作者表示第17章／全17章・Lean
融通のきかない審査官
感動的な演説は、証明項の代わりにならない。
ここまでと、この先
矛盾まで読んで、数学の道筋が一周しました。最後は、その道筋を理解すること、Leanの原文を見ること、Leanのカーネルで実際に検査することを区別します。このサイトを読むだけで、その全検査を実行したことにはなりません。
このつながりは、読む道筋の案内です。物語のたとえ自体が、この定理の証明になるわけではありません。
まず、この言葉から
知っている言葉は飛ばして大丈夫。初めてなら、言葉を開くか、基礎から順に読んでみよう。
この章を基礎から順に説明して →物語 → 証明フクロウの点検は#print axioms。定理がどの基礎的な公理に依存するかLeanに尋ねます。拍手は証拠になりません。
公理への依存を調べる#print axioms fermat_last_theoremミカ
「証言台に三つの形:propext、Classical.choice、Quot.sound。法廷の土台であって、FLTについての信じごとではありません。」
土台も確認物語 → 証明三つの形はpropext・Classical.choice・Quot.sound。基礎となる公理であり、FLTが正しいと仮定したものではありません。
報告された基礎を読むpropext, Classical.choice, Quot.soundピップ
「これで閉廷:主張の形は望んだ形と一致、自然数と正の数の証拠つき。事件ファイル:検査済みです。」
次の一歩へ物語 → 証明本を閉じる前に主張の形も合わせます。自然数では、0ではないという証拠から正であることが得られます。
非零から正へNat.pos_of_ne_zero ha物語の向こうにある考え方
#guard_msgsが#print axioms fermat_last_theoremの診断を検査します。flt_pinnedは明示的な型の主張を、flt_mathlibはMathlibのFermatLastTheoremを実現します。原文のスナップショットはカーネル検査の結果ではないので、このアプリではFLTをローカル検証済みとは表示しません。
FLT全体に新しい「ローカル検証済み」表示をつけられるのは？
- 必要な依存先とツールチェーンをそろえ、固定版の検査が実際に成功したとき。
- 原文の#print axiomsを目で読んだとき。
このページで物語と原文を読めます。証明の編集、クイズ、対話式のマップにはJavaScriptを有効にしてください。
練習用のリアルタイム検査
証明の続きを、あなたの手で。
小さな場面、本物の論理の目標。そして、あなたの成功を気にかけるハト。
事件簿を開いています…