通っても、言いたいことが言えているか — 検査が通ることと、問題を書けていること

Lean が「通った」と言うのは、書いた言明が書いた証明から出るということだけです。書いた言明が解きたかった問題かどうかは、Lean は見ていません。定義を一文字変えれば別の主張になり、それでも証明は通ることがあります。

この隙間の落ち方には、繰り返し出てくる型が四つあります。型ごとに、実際に検査して通った小さな例と、機械検査済みの成果の中に現れた実例を対にして並べます。

このページの Lean のコードは、通る例も通らない例も、すべて手元で検査したものです。Lean 4（v4.33.1）と mathlib を使っています。

小さな例 — 素数の定義から「2 以上」を落とす

素数を「1 と自分自身以外に約数を持たない数」と説明することがあります。これをそのまま Lean に書き写します。∀ m ≤ n と上限を付けたのは、判定を有限にして decide に載せるためで、n ≥ 1 なら約数は必ず n 以下ですから条件は変わりません。

def MyPrime (n : ℕ) : Prop := ∀ m ≤ n, m ∣ n → m = 1 ∨ m = n

この定義に 1 を入れます。1 の約数は 1 だけで、それは「1 または n」に当てはまるので、条件は満たされます。

theorem myPrime_one : MyPrime 1 := by decide
theorem not_prime_one : ¬ Nat.Prime 1 := by decide

二行とも通ります。つまり MyPrime は mathlib の Nat.Prime とは違う述語です。7 では両方が同じ答えを出すので、いくつか試しただけでは気づきません。

theorem both_seven : MyPrime 7 ∧ Nat.Prime 7 := by decide

直すには 2 ≤ n を足します。そして直したあとに、直った定義が元から在る定義と一致することを、有限の範囲で確かめさせます。

theorem fixed_agrees : ∀ n ≤ 20, ((2 ≤ n ∧ MyPrime n) ↔ Nat.Prime n) := by decide

最後の一行が効きます。20 までの一致は証明ではありませんが、書き間違いはここで落ちます。新しく書いた定義には、既に在る定義との一致を有限の範囲で当てる行を添えておくとよいでしょう。

実例 — 単位距離グラフの「置ける」に、弱い版と強い版がある

単位距離グラフは、平面上の相異なる点を頂点とし、辺で結ばれた二点の距離がちょうど 1 のものです。与えられたグラフがそういう形で平面に置けるかを問います。この「置ける」を Lean に書くとき、二通りの定義が出てきます。

弱い版は、辺で結ばれた二点の距離が 1 であることだけを要求し、辺でない二点の距離には何も言いません。証明書の組み方で使っているのがこの形です。

/-- 辺の条件だけ（非辺には何も課さない・単射性も課さない）。 -/
def Edges (E : List (ℕ × ℕ)) (x y : ℕ → ℝ) : Prop :=
  ∀ e ∈ E, (x e.1 - x e.2)^2 + (y e.1 - y e.2)^2 = 1

強い版は、辺 ⟺ 距離 1 の両向きを要求します。辺でない二点は距離 1 であってはいけません。この二つは同じ言葉で呼ばれるのに、別の述語です。小さな絵で差が出ます。

/-- 距離の二乗（平方根を避けるため、実現は二乗で書く）。 -/
def sq2 (a b : ℝ × ℝ) : ℝ := (a.1 - b.1) ^ 2 + (a.2 - b.2) ^ 2

/-- **弱い版**：辺で結ばれた二点は距離 1。非辺には何も課さない。 -/
def WeakReal (E : List (ℕ × ℕ)) (p : ℕ → ℝ × ℝ) : Prop :=
  ∀ e ∈ E, sq2 (p e.1) (p e.2) = 1

/-- **強い版**：`n` 点の範囲で、辺 ⟺ 距離 1。 -/
def FaithReal (n : ℕ) (E : List (ℕ × ℕ)) (p : ℕ → ℝ × ℝ) : Prop :=
  ∀ i < n, ∀ j < n, i ≠ j → ((((i, j) ∈ E) ∨ ((j, i) ∈ E)) ↔ sq2 (p i) (p j) = 1)

中心から 6 本の輻だけを辺にし、正六角形の外周は辺にしないグラフを取ります。絵のほうは、中心とその周りの単位正六角形という普通の配置にします（s は √3 / 2）。

def hexE : List (ℕ × ℕ) := [(0, 1), (0, 2), (0, 3), (0, 4), (0, 5), (0, 6)]

noncomputable def hexP : ℕ → ℝ × ℝ
  | 1 => (1, 0)
  | 2 => (1 / 2, s)
  | 3 => (-(1 / 2), s)
  | 4 => (-1, 0)
  | 5 => (-(1 / 2), -s)
  | 6 => (1 / 2, -s)
  | _ => (0, 0)

この絵は弱い版を満たしますが、強い版は満たしません。隣り合う外周の二点が、辺で結ばれていないのに距離 1 にあるからです。

theorem hex_weak : WeakReal hexE hexP
theorem hex_not_faith : ¬ FaithReal 7 hexE hexP

二つの定義をつなぐ向きは、次の一本だけです。強い版で置けたなら弱い版でも置けている。逆は上の例のとおり成り立ちません。

theorem weak_of_faith (n : ℕ) (E : List (ℕ × ℕ))
    (hE : ∀ e ∈ E, e.1 < n ∧ e.2 < n ∧ e.1 ≠ e.2) (p : ℕ → ℝ × ℝ)
    (h : FaithReal n E p) : WeakReal E p

theorem no_faith_of_no_weak (n : ℕ) (E : List (ℕ × ℕ))
    (hE : ∀ e ∈ E, e.1 < n ∧ e.2 < n ∧ e.1 ≠ e.2)
    (h : ∀ p : ℕ → ℝ × ℝ, ¬ WeakReal E p) :
    ∀ p : ℕ → ℝ × ℝ, ¬ FaithReal n E p

ここから、どちらの定義を使うかが目的で決まります。

「実現」という一つの言葉の下に二つの定義が並び、両者をつなぐ橋が一本必要になります。これは Lean に書いて初めて見えたことで、紙の上では「置ける」の一語で通り過ぎていました。機械検査済みの側では、置けないことの証明書は弱い版（Edges・Realiz）で書かれており、上界の議論に使う部品は強い版を前提にしています。両者は今のところ別の定理で、橋は掛かっていません。

小さな例 — 「一覧の全部が条件を満たす」と「条件を満たすものは一覧に全部在る」

素数を三つ挙げた一覧を作り、その全部が素数であることを証明します。一覧の長さも数えます。

def cand : List ℕ := [2, 3, 5]

theorem cand_all_prime : ∀ n ∈ cand, Nat.Prime n := by decide
theorem cand_card : cand.length = 3 := by decide

二行とも通ります。しかしどちらも「素数はこの一覧で尽きている」とは言っていません。7 が抜けています。

theorem cand_not_complete : ¬ (∀ n, Nat.Prime n → n ∈ cand) := by
  intro h
  have h7 := h 7 (by decide)
  revert h7
  decide

これも通ります。つまり cand_all_prime と cand_card は、cand_not_complete と同時に成り立ちます。前二つを見て「素数を全部押さえた」と読むのが誤りです。

実例 — 「117 類はどれも置けない」は「候補は 117 類で全部」ではない

単位距離グラフの側に、同じ形の言明があります。11 点で独立数が 3 以下の候補を列挙し、その一つ一つについて平面に置けないことを証明した定理です。

theorem hn11_no_realiz : ∀ E ∈ cands, ∀ p : Fin 11 → ℝ × ℝ, ¬ Realiz E p
theorem cands_card : cands.length = 117 := by decide

この二本が言っているのは、cands に挙げた 117 個の辺集合はどれも平面に単位距離で置けないことと、cands の長さは 117 であることです。「11 点で独立数 3 以下のグラフは cands の 117 類で尽きている」——列挙の完全性は、この二本のどこにも入っていません。完全性は Lean の外側の計算で確かめたもので、等級は 計算 です。

定理名は短いほうが読みやすいのですが、短い名前は言明より広い読みを誘います。hn11_no_realiz という名前からは「11 点の場合は片付いた」と読めてしまいます。名前ではなく言明を読む必要があり、その手順を 09 言明を読む手順に書きました。

小さな例 — 仮定が偽なら、結論は何でもよい

偽の仮定を置いた定理は、結論に何を書いても通ります。

theorem foo (h : 2 + 2 = 5) : 0 = 1 := by omega

空集合の上の「すべての元について」も、中身を確かめずに通ります。

theorem bar : ∀ x ∈ (∅ : Finset ℕ), x = x + 1 := by decide

この二本に #print axioms（その定理が依拠する公理を並べる命令）を当てると、次が出ます。

'G08.foo' depends on axioms: [propext, Quot.sound]
'G08.bar' depends on axioms: [propext, Classical.choice, Quot.sound]

どちらも標準の三公理の内側で、sorryAx（未証明の穴）も出ません。公理の欄がきれいであることは、言明が空虚でないことを何も保証しません。foo のほうは公理が二つしか出ておらず、三つ出る定理より「きれい」に見えますが、中身はありません。

対策 — 非空性の確認と陰性対照を Lean の中に置く

空虚に真であること自体は誤りではありません。誤りになるのは、空虚だと気づかないまま「成り立つ」と読むときです。機械検査済みの側では、次の三つの形で対策が入っています。

/-- `L = 4` で仮定が満たされること（定理が空でない）。 -/
example (x : V 4) (μ ν : Fin 4) (h : μ ≠ ν) :
    ∃! e : Edge 4, InP e x μ ν ∧ Istar (L := 4) ⟨2, rfl⟩ e :=
  plaq_unique _ x μ ν h

example (e : Rest (L := 4) ⟨2, rfl⟩) :
    (Finset.univ.filter (fun s => e ∈ Es (L := 4) ⟨2, rfl⟩ s)).card = 6 :=
  star_count _ (two_ne_zero_of_le (by norm_num)) e

/-- 原点から方向 3 の辺は `I*`（`x₁ = x₂ = x₄`）：star の族は空でない。 -/
example : Istar (L := 4) ⟨2, rfl⟩ ((0 : V 4), (2 : Fin 4)) := by
  unfold Istar red
  simp only [Pi.zero_apply, map_zero]
  decide

最後の一本が「族そのものが空でない」を言っています。族が空なら「族のどの辺も…」は空虚に真になります。

/-- 陰性対照：空の族は完全でない（`d = 3`）。 -/
theorem not_perfect_empty3 : ¬ Perfect (fun (_ : Fin 3) (_ : V 3) => false) := by decide

/-- 陰性対照：全部の辺をとった族は完全でない（`d = 3`）。 -/
theorem not_perfect_full3 : ¬ Perfect (fun (_ : Fin 3) (_ : V 3) => true) := by decide

/-- 陰性対照：`I4` の方向 0 を全部に替えると完全でなくなる（`d = 4`）。 -/
theorem not_perfect_I4_broken :
    ¬ Perfect (fun (μ : Fin 4) (x : V 4) => if μ = 0 then true else I4 μ x) := by decide

三本目が効きます。正解を一箇所だけ壊した族を入れて、判定が落ちることを見ます。空の族と満杯の族が落ちるだけなら、判定が粗くても通ってしまいます。

同じファイルには、逆に空虚に真であることを定理として明記した行もあります。

/-- `d ≤ 1` には 2 次元の面が無いので、どんな族も完全（空虚に真）。 -/
theorem perfect_of_le_one {d : ℕ} (hd : d ≤ 1) (I : Fin d → V d → Bool) : Perfect I

これは「d ≤ 1 でも完全な族がある」という発見ではなく、その次元では言明に中身が無いという注意です。空虚な範囲に名前を付けて括り出しておけば、結論の読み間違いが起きません。

structure IsHaarS3 (μ : Measure ℍ[ℝ]) : Prop where
  prob : IsProbabilityMeasure μ
  unit : ∀ᵐ u ∂μ, ‖u‖ = 1
  inv : ∀ q : ℍ[ℝ], ‖q‖ = 1 → μ.map (fun u => q * u) = μ

この三条件（全確率が 1・ほとんどの点がノルム 1・単位ノルムの元を左から掛けても変わらない）で「3 次元球面の上の一様な測度」を指しています。これを満たす測度を具体的に作り、条件を満たすことを示した定理があります。

theorem isHaarS3_haarS3 : IsHaarS3 haarS3

haarS3 は、ルベーグ測度を単位球に制限して x ↦ x/‖x‖ で押し出し、全体を 1 に正規化したものです。この一本があるので、IsHaarS3 μ を仮定した定理はすべて空虚ではありません。性質で定義したら、その性質を持つ具体物を一つ作る——この組が要ります。

大きな主張を Lean に載せるとき、扱いにくい部分を先に仮定へ追い出して、残りだけを閉じることがよくあります。そのとき定理は「仮定つき」のまま存在します。仮定が誰かによって満たされるまで、結論だけを引くことはできません。

実例 — 「どの辺もちょうど 6 個の star に入る」が仮定から消えるまで

格子ゲージ理論の有効作用について、二階微分の下界を示す定理があります。最初の形では、格子の幾何をすべて仮定に追い出した抽象的な言明でした。h6 がその中心で、「どの辺もちょうど 6 個の star に入る」という格子の性質を、証明せずに仮定として受け取っています。

theorem hess_star_family {S E : Type*} [Fintype S] [Fintype E] [DecidableEq E]
    (Es : S → Finset E) (h6 : ∀ e, (univ.filter (fun s => e ∈ Es s)).card = 6)
    (x : E → ℝ) (hx : ∀ e, 0 ≤ x e) (β : ℝ)
    (q A B C : S → Fin 6 → ℍ[ℝ]) (hq : ∀ s i, ‖q s i‖ = 1)
    (hA : ∀ s i, (A s i).re = 0) (hB : ∀ s i, (B s i).re = 0) (hC : ∀ s i, (C s i).re = 0)
    (hslot : ∀ s, ∑ i, (‖A s i‖ ^ 2 + ‖B s i‖ ^ 2 + ‖C s i‖ ^ 2) ≤ ∑ e ∈ Es s, x e) :
    -(27 * β ^ 2) * ∑ e, x e ≤
      deriv (deriv (fun τ => ∑ s, -G β (‖∑ i, curve (q s i) (A s i) (B s i) (C s i) τ‖ ^ 2))) 0

仮定が九つ並んでいます。この段階で「二階微分の下界が Lean で閉じた」と言うと、九つの仮定を満たす格子があるかどうかを言わずに結論だけを渡すことになります。

次の段で、具体的な格子について h6 が本当に成り立つことを示した定理が入りました。

theorem star_count (hL : (2 : ZMod L) ≠ 0) (e : Rest h2) :
    (univ.filter (fun s => e ∈ Es h2 s)).card = 6

さらに次の段で、摂動の形を格子の言葉に書き直して、残りの仮定も消えました。最後の形の仮定は、場の型と周期の条件だけです。

theorem hess_gauge [NeZero L] (h2 : 2 ∣ L) (hL : 3 ≤ L) (U X : Rest h2 → ℍ[ℝ])
    (hU : ∀ e, ‖U e‖ = 1) (hX : ∀ e, (X e).re = 0) (β : ℝ) :
    -(27 * β ^ 2) * ∑ e, ‖X e‖ ^ 2 ≤
      deriv (deriv (fun τ => Phi h2 (two_ne_zero_of_le hL) β (pert h2 U X τ))) 0

2 ∣ L（周期が偶数）・3 ≤ L・‖U e‖ = 1（場が単位四元数）・(X e).re = 0（摂動の生成子が純虚）。この四つは「格子ゲージ理論の配位である」ことそのもので、追い出した仮定ではありません。

「Lean で閉じた」と言うときは、仮定の一覧を一緒に言います。三つの段はどれも「二階微分の下界」を述べていますが、読み手が使える範囲はまったく違います。

四つの型に共通の対策が一つあります。ひとまとまりの結果について「どこまでが Lean で、どこからが紙で、どこが計算か」を表にして、結果と一緒に置くこと。表を作る作業そのものが、上の四つを洗い出します。

札の意味はサイト共通です。

Lean機械検査済み（標準三公理以下・sorryAx なし・定理名を添える） 紙証明はあるが機械検査は未了 計算手元で確かめた範囲。外に出す主張にはしない 既知言い換え・既知の定理・外の文献の確認

例 1 — 単位距離グラフの側

上の三段だけを見ると上界も下界も機械検査済みに見えますが、上界には四段目が要ります。表にすると、要る行が抜けていることが目で見えます。

例 2 — 格子ゲージ理論の側

以下は強結合域の定数についての話で、連続極限や質量ギャップ問題の本体への主張はありません。

この表では、Lean の行と紙の行の継ぎ目が一箇所に見えます——二階微分の下界（Lean）から曲率の下界（紙）へ渡るところです。継ぎ目を隠さずに書けば、読み手はそこを自分で検分できます。

次は 09 言明を読む手順——このページの四つを、結果を受け取る側のチェックリストにしたものです。用語は 12 用語集。