証明書を Lean に検査させる — 探すのは外の計算、確かめるのは Lean

指定した辺の両端の距離がすべて 1 になるように、11 個の点を平面に置けるか。
（単位距離グラフ：平面の点を頂点とし、距離がちょうど 1 の二点を辺で結んだグラフ。ここでは辺の両端だけに距離 1 を課し、辺でない対には何も課しません。）

置けない、というのが答えです。ある 117 個の辺リストのどれについても置けません。この「置けない」を機械に確かめさせるには、どう渡せばよいかがこのページの主題です。

難しいのは、置き方が連続無限にあることです。03 の decide は場合を全部並べられるときにしか使えませんし、探索そのものを Lean に書かせると、探索の効率の話が証明の中に混ざります。分けます。

やり方は二つに分かれます。

• 外の計算が、証明書を探す。区間演算で場合を分けながら「この置き方はできない」を潰していき、潰し方の記録を残します。速さが命なので、道具は何でもよく——数値計算の言語でも、探索の工夫でも、当てずっぽうでも構いません。間違っていても構いません。
• Lean が、証明書を検査する。証明書を読んで「たしかに潰れている」を確かめる関数を Lean で書き、その関数が真を返すなら実現は無いという定理を証明します。証明書が間違っていれば検査が偽を返すので、外の計算を信じる必要がありません。

信じるのは検査器の健全性の証明だけです。探索の正しさは信じません。この分け方の利点は二つあります。探索を好きなだけ速くできること、そして探索を書き換えても Lean の側を書き換えなくて済むことです。

証明書を検査させる組み方は、いつも四段です。①データの形・②検査する関数・③健全性の定理・④個別の証明書を decide で回す。この四段だけを、中身を取り替えて小さく書くとこうなります。

import Mathlib

/-! 証明書を検査させる四段の、いちばん小さな形。 -/

/-- ① 証明書の形（データ）。端点が整数の区間。 -/
structure Box where
  lo : ℤ
  hi : ℤ

/-- ② 検査する関数。整数の比較だけで「この箱は 1 を含まない」と言う。 -/
def excludesOne (b : Box) : Bool := decide (b.hi < 1) || decide (1 < b.lo)

/-- ③ 健全性の定理。検査が `true` なら、その箱に入る実数は 1 ではない。 -/
theorem excludesOne_sound {b : Box} {x : ℝ}
    (hb : excludesOne b = true) (h1 : (b.lo : ℝ) ≤ x) (h2 : x ≤ (b.hi : ℝ)) : x ≠ 1 := by
  rcases Bool.or_eq_true_iff.1 hb with h | h
  · have : (b.hi : ℤ) < 1 := of_decide_eq_true h
    have : (b.hi : ℝ) < 1 := by exact_mod_cast this
    intro hx; rw [hx] at h2; linarith
  · have : (1 : ℤ) < b.lo := of_decide_eq_true h
    have : (1 : ℝ) < (b.lo : ℝ) := by exact_mod_cast this
    intro hx; rw [hx] at h1; linarith

/-- ④ 個別の証明書を `decide` で回す。 -/
theorem box_ok : excludesOne ⟨2, 5⟩ = true := by decide

/-- 二つを繋ぐと、外の計算が出した箱について Lean が結論を出す。 -/
example {x : ℝ} (h1 : (2 : ℝ) ≤ x) (h2 : x ≤ 5) : x ≠ 1 :=
  excludesOne_sound box_ok h1 h2

Lean手元で検査して通ったもの。見どころは、③の定理が実数について語り、④の計算が整数しか触っていないことです。実数の主張と、計算できるデータの間に橋を架けるのが③の役目で、それが済めば④はいくら増やしても同じ形で足せます。

以下は、この四段の中身を本物に取り替えたものです。

平方根を式から消す

三点の距離から座標を決める操作（三辺測量）には、素直に書くと平方根が出ます。平方根が式に入ると、区間演算も比較も一気に重くなります。

そこで一歩を二つに割ります。頂点 v が既に置いた a, b の双方から距離 1 のとき、u := v − (a+b)/2・d := b − a と置けば u と d は直交し、u は d を 90 度回したベクトルの実数倍になります。その倍率を lam と呼ぶと、|d|²(4 lam² + 1) = 4 が成り立ちます。

/-- **`trilat_core`**：`u ⊥ d`・`d ≠ 0` なら `u` は `d` の直交方向 `(−d_y, d_x)` の実数倍。 -/
lemma trilat_core {ux uy dx dy : ℝ} (hD : dx^2 + dy^2 ≠ 0) (hlin : ux*dx + uy*dy = 0) :
    ∃ lam : ℝ, ux = -(lam*dy) ∧ uy = lam*dx

lam の上下界は、平方根を取らずに整数の掛け算だけで検査できます。証明書が上下界の 2 整数を差し出し、Lean はそれが |d|²(4 lam² + 1) = 4 と両立することを掛け算で検めます。

/-- **`lam_box`**：`|d|²·(4 lam² + 1) = 4` と `|d|²` の区間から `lam` の箱を二つ出す。
平方根は現れず、検査は `ℤ` の掛け算だけ。 -/
lemma lam_box {lam D : ℝ} {dl dh ll lu : ℤ}
    (hD1 : (dl:ℝ) ≤ (sc:ℝ) * D) (hD2 : (sc:ℝ) * D ≤ (dh:ℝ)) (hdl : 0 < dl)
    (heq : D * (4*lam^2 + 1) = 4)
    (hll : 0 ≤ ll) (hlu : ll ≤ lu)
    (hU : sc*sc*(4*sc - dl) ≤ 4*dl*lu*lu)
    (hL : ll = 0 ∨ 4*dh*ll*ll ≤ sc*sc*(4*sc - dh)) :
    Sem ⟨ll, lu⟩ lam ∨ Sem ⟨-lu, -ll⟩ lam

結論が「または」になっているのが要点です。lam は正の側か負の側のどちらかにある——これが分枝の木の二股になります。

区間の端点を整数にする

区間演算の端点は、実数でも有理数でもなく整数にしました。実数では計算できず、有理数では分母が掛け算のたびに膨らみます。整数なら kernel の評価が整数の加減乗と比較だけで終わります。

小数を扱うために、尺度 2^40 の固定小数点を使います。「区間 I が実数 x を含む」という意味づけを定義し、演算ごとに健全性を証明します。

/-- 固定小数点の尺度 `2^40`。リテラルで書くのは核の評価を速くするため。 -/
def sc : ℤ := 1099511627776

/-- 端点が `ℤ`（尺度 `sc`）の閉区間。 -/
structure Ivl where
  lo : ℤ
  hi : ℤ
deriving DecidableEq

/-- `x` が区間 `I` に入る：`I.lo ≤ sc·x ≤ I.hi`。 -/
def Sem (I : Ivl) (x : ℝ) : Prop := (I.lo : ℝ) ≤ (sc:ℝ) * x ∧ (sc:ℝ) * x ≤ (I.hi : ℝ)

def addI (a b : Ivl) : Ivl := ⟨a.lo + b.lo, a.hi + b.hi⟩

def subI (a b : Ivl) : Ivl := ⟨a.lo - b.hi, a.hi - b.lo⟩

def mulI (a b : Ivl) : Ivl :=
  ⟨(min (min (a.lo*b.lo) (a.lo*b.hi)) (min (a.hi*b.lo) (a.hi*b.hi))) / sc,
   -((-(max (max (a.lo*b.lo) (a.lo*b.hi)) (max (a.hi*b.lo) (a.hi*b.hi)))) / sc)⟩

lemma addI_sound {a b : Ivl} {x y : ℝ} (ha : Sem a x) (hb : Sem b y) : Sem (addI a b) (x + y)

lemma mulI_sound {a b : Ivl} {x y : ℝ} (ha : Sem a x) (hb : Sem b y) : Sem (mulI a b) (x * y)

加減は厳密で、乗算だけが丸めを起こします。mulI の / sc が切り捨て、もう一方が切り上げになっていて、区間が外向きに広がります。外向きであることが健全性（mulI_sound）の内容で、内向きに丸めると偽の棄却が出ます。

辺をリストにする

グラフは SimpleGraph ではなく List (ℕ × ℕ)——頂点番号の対の並び——にしました。証明書を decide で回すため、辺の所属が計算できる形である必要があります。実現の定義は二段に分けます。

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

/-- `E` を辺集合とする 11 点グラフの平面単位距離実現：
  辺は距離 1・**非辺は制約なし**・異なる頂点は異なる点。 -/
def Realiz (E : List (ℕ × ℕ)) (p : Fin 11 → ℝ × ℝ) : Prop :=
  (∀ e ∈ E, ((p (emb e.1)).1 - (p (emb e.2)).1)^2
      + ((p (emb e.1)).2 - (p (emb e.2)).2)^2 = 1) ∧ Function.Injective p

Edges のほうが条件が弱い（点が重なってもよい）ので、Edges で否定が出れば Realiz の否定も出ます。弱い側で閉じられるなら、そちらで閉じておく——あとで強い側に降ろすのは一行です。

座標系を固定する

平面の置き方は回転と平行移動で動くので、辺 1 本を (0,0)–(1,0) に固定します。これは一般性を失わないことを証明しておく必要があり、Lean では回転の式を具体的に書いて等式を確かめます。

/-- **正規化**：辺 `ab` があれば、回転と平行移動で `a = (0,0)`・`b = (1,0)` にできる。 -/
lemma normalize (E : List (ℕ × ℕ)) (a b : ℕ) (hab : (a, b) ∈ E) (x y : ℕ → ℝ)
    (h : Edges E x y) :
    ∃ X Y : ℕ → ℝ, Edges E X Y ∧ X a = 0 ∧ Y a = 0 ∧ X b = 1 ∧ Y b = 0

①証明書の形。分枝の木です。箱は運びません——検査器が自分で計算します。運ぶのは木の形と、各分枝での lam の上下界（整数 2 個）、二分の位置だけです。

inductive Tr where
  | kill (u w : ℕ) : Tr
  | split (ll lu : ℤ) (tp tm : Tr) : Tr
  | bisx (v : ℕ) (mid : ℤ) (t1 t2 : Tr) : Tr
  | bisy (v : ℕ) (mid : ℤ) (t1 t2 : Tr) : Tr
  | free (u p : ℕ) (t : Tr) : Tr

五つの枝の意味。split は三辺測量の一歩で、lam の符号で二股に分かれます。kill は「この辺の長さの区間が 1 を含まないので、ここは潰れた」。bisx・bisy は箱をその軸で二分する（明らかに健全）。free は辺の片端を相手のまわりの [-1,1]² に置く段で、角度が自由なときに使います。

②検査する関数。Bool を返します。

def chk (E : List (ℕ × ℕ)) : Tr → List (ℕ × ℕ × ℕ) → St → Bool
  | .kill u w, _, σ =>
      match σ u, σ w with
      | some A, some B => isEdge E u w && killOK A B
      | _, _ => false
  | .split ll lu tp tm, pl, σ =>
      match pl with
      | [] => false
      | (v, a, b) :: pl' =>
          match σ a, σ b with
          | some A, some B =>
              isEdge E v a && isEdge E v b && (triStep ll lu A B).1 &&
                chk E tp pl' (upd σ v (triStep ll lu A B).2.1) &&
                chk E tm pl' (upd σ v (triStep ll lu A B).2.2)
          | _, _ => false
  | .bisx v mid t1 t2, pl, σ =>
      match σ v with
      | some A =>
          chk E t1 pl (upd σ v (⟨A.1.lo, mid⟩, A.2)) &&
            chk E t2 pl (upd σ v (⟨mid, A.1.hi⟩, A.2))
      | none => false

（bisy と free の枝も同じ形です。）この関数は証明ではありません。単に Bool を計算するプログラムで、間違った証明書を渡せば false を返します。

③健全性の定理。ここが分業の要です。

/-- **検査器の健全性**：`chk` が `true` を返せば、その状態を満たす実現は存在しない。 -/
theorem chk_sound (E : List (ℕ × ℕ)) (x y : ℕ → ℝ) (hE : Edges E x y) :
    ∀ (t : Tr) (pl : List (ℕ × ℕ × ℕ)) (σ : St), Holds σ x y → chk E t pl σ = true → False

証明は Tr の構造についての帰納法です。枝が五つあるので五つの場合を埋めることになり、それぞれで「区間演算の健全性」と「三辺測量の一歩の健全性」を使います。ここを一度証明すれば、証明書がいくつ増えても再証明は要りません。

座標系の固定と組み合わせると、候補を閉じる道具になります。

/-- **候補を閉じる道具**：証明書 `t`・平面 `pl` の検査が通れば辺の条件を満たす座標は無い。 -/
theorem close_edges (E : List (ℕ × ℕ)) (a b : ℕ) (hab : (a, b) ∈ E) (t : Tr)
    (pl : List (ℕ × ℕ × ℕ)) (hchk : chk E t pl (st0 a b) = true) :
    ∀ x y : ℕ → ℝ, ¬ Edges E x y := by
  intro x y h
  obtain ⟨X, Y, hXY, h1, h2, h3, h4⟩ := normalize E a b hab x y h
  exact chk_sound E X Y hXY t pl (st0 a b) (holds_st0 h1 h2 h3 h4) hchk

Leantrilat_core・lam_box・mulI_sound・chk_sound・normalize・close_edges・close_realiz。

④ここからは機械的です。候補ごとに、辺リスト・三辺測量の順序・証明書の木を並べ、decide で回します。

def E0 : List (ℕ × ℕ) := [(0, 1), (0, 2), (0, 3), (1, 2), (1, 6), (1, 10), (2, 7), (2, 10), (3, 8), (3, 9), (4, 5), (4, 6), (4, 7), (4, 8), (5, 6), (5, 7), (5, 9), (6, 8), (6, 10), (7, 9), (8, 10), (9, 10)]

def pl0 : List (ℕ × ℕ × ℕ) := [(6, 4, 5), (7, 4, 5), (8, 4, 6), (9, 5, 7), (10, 6, 8), (1, 6, 10), (2, 1, 10), (0, 1, 2), (3, 0, 8)]

theorem chk0 : chk E0 tr0 pl0 (st0 4 5) = true := by decide +kernel

theorem no_edges_0 : ∀ x y : ℕ → ℝ, ¬ Edges E0 x y :=
  close_edges E0 4 5 (by decide) tr0 pl0 chk0

theorem no_realiz_0 : ∀ p : Fin 11 → ℝ × ℝ, ¬ Realiz E0 p :=
  close_realiz E0 4 5 (by decide) tr0 pl0 chk0

pl0 が三辺測量の順序（「頂点 6 を 4 と 5 から、頂点 7 を 4 と 5 から、…」）、tr0 が分枝の木です。tr0 は .split と .kill が入れ子になった一行で、952205001410 のような整数が lam の下界・上界です（尺度 2^40 なので、実数に直すと 0.8660… のあたり）。この一行を書いたのは外の計算で、Lean はそれを読んで検めるだけです。

def tr0 : Tr := .split 952205001410 952205001411 (.split 952205001410 952205001411 (.split 952205001409 952205001411 (.split 952205001409 952205001411 (.split 952205001406 952205001414 (.kill 10 9) (.kill 10 9)) (.split 952205001406 952205001414 (.kill 10 9) (.kill 10 9))) (.split 952205001409 952205001411 (.split 952205001406 952205001415 (.kill 10 9) (.kill 10 9)) (.split 952205001406 952205001415 (.kill 10 9) (.kill 10 9)))) (.split 952205001409 952205001411 (.split 952205001409 952205001411 (.split 952205001406 952205001414 (.kill 10 9) (.kill 10 9)) (.split 952205001406 952205001414 (.kill 10 9) (.kill 10 9))) (.split 952205001409 952205001411 (.split 952205001406 952205001415 (.kill 10 9) (.kill 10 9)) (.split 952205001406 952205001415 (.kill 10 9) (.kill 10 9))))) (.split 952205001410 952205001411 (.split 952205001409 952205001411 (.split 952205001409 952205001411 (.split 952205001406 952205001415 (.kill 10 9) (.kill 10 9)) (.split 952205001406 952205001415 (.kill 10 9) (.kill 10 9))) (.split 952205001409 952205001411 (.split 952205001406 952205001414 (.kill 10 9) (.kill 10 9)) (.split 952205001406 952205001414 (.kill 10 9) (.kill 10 9)))) (.split 952205001409 952205001411 (.split 952205001409 952205001411 (.split 952205001406 952205001415 (.kill 10 9) (.kill 10 9)) (.split 952205001406 952205001415 (.kill 10 9) (.kill 10 9))) (.split 952205001409 952205001411 (.split 952205001406 952205001414 (.kill 10 9) (.kill 10 9)) (.split 952205001406 952205001414 (.kill 10 9) (.kill 10 9)))))

decide +kernel は「kernel の評価だけで判定する」という指定です。通常の decide は途中で tactic 側の評価器も使いますが、大きな計算では kernel に直接やらせるほうが速く、しかも信頼の範囲は kernel のままです（native_decide とは違います）。

117 個を並べ終えると、全体の定理が一本になります。

/-- **主定理**：`cands`（117 類）のどの辺集合も平面に単位距離で実現しない。 -/
theorem hn11_no_realiz : ∀ E ∈ cands, ∀ p : Fin 11 → ℝ × ℝ, ¬ Realiz E p

/-- 辺の条件だけの版（単射性を使わない・より強い）。 -/
theorem hn11_no_edges : ∀ E ∈ cands, ∀ x y : ℕ → ℝ, ¬ Edges E x y

/-- 候補は 117 個。 -/
theorem cands_card : cands.length = 117 := by decide

Leanhn11_no_realiz・hn11_no_edges・cands_card。節点は全部で 34,049・CPU は 11 分でした。計算

'hn11_no_realiz' depends on axioms: [propext, Classical.choice, Quot.sound]
'hn11_no_edges' depends on axioms: [propext, Classical.choice, Quot.sound]
'cands_card' does not depend on any axioms
'trilat_core' depends on axioms: [propext, Classical.choice, Quot.sound]
'lam_box' depends on axioms: [propext, Classical.choice, Quot.sound]
'chk_sound' depends on axioms: [propext, Classical.choice, Quot.sound]
'chk0' depends on axioms: [propext, Quot.sound]

読みどころが二つ。chk0（証明書の検査そのもの）に Classical.choice が出ていません。kernel の評価で閉じているので、選択公理が要らないのです。cands_card は公理をまったく使いません——リストの長さを数えるだけだからです。

そして sorryAx と Lean.ofReduceBool はどこにも出ません。decide +kernel は native_decide ではないので、公理は増えません。ここが「速くしたいが信頼の範囲は広げない」の線です。

同じ型の仕事で、16 点の 2,100 個の候補と、途中のフィルタが捨てた 10 点の 296 個の候補も Lean に入っています（hn16_no_realiz・hn10_no_realiz）。検査器（chk とその健全性）は書き換えていません。頂点の個数に依らないように作ったので、候補の側を足すだけで済みました。

ここを一度はっきり書きます。Lean が保証しているのは「挙げた候補が置けない」までで、「候補がそれで全部」は保証していません。

Lean にある言明は二本です。

この二本から言えるのは「117 個の具体的な辺リストについて実現しない」だけです。「条件を満たす 11 点グラフの同型類が、ちょうどこの 117 個である」は Lean の外にあります。それは列挙の計算で、辺の個数や次数の下限で枝を刈りながら同型類を作り、同型判定で重複を落とす——という手続きの正しさに依っています。

だから、この題材から出る上界の主張は次の形で書くことになります。

証明書は Lean・完全性は計算。

実際、16 点の側では埋まっていない箇所が三つあります——列挙の完全性、途中のフィルタの健全性の組合せの部分、枡ごとの同型判定です。幾何の側（実現しないこと）は Lean に入り、組合せの側（候補が全部であること）は計算のままです。この線を書かずに「Lean で証明した」と言うと、言っていないことを言ったことになります。

穴を埋める道がないわけではありません。列挙そのものを Lean の中で回せば閉じますが、そのときは「列挙器の健全性」と「列挙器の完全性」の両方を証明する必要があり、後者は前者よりずっと重い仕事になります。健全性（言ったことは正しい）と完全性（全部言った）は、形式化の重さが違います。

hn11_no_realiz が言っているのは次のことです。

リスト cands の各要素 E について、Fin 11 から平面への写像 p で「E の各辺の両端の距離が 1」かつ「p が単射」を満たすものは、一つも存在しない。

言っていないことを四つ。

• 「候補がそれで全部」とは言っていません。§08 の通りです。
• 「辺でない対の距離が 1 でない」とは言っていません。Realiz は辺だけに距離 1 を課します。単位距離グラフの定義としてはこれで正しいのですが（辺でない対が偶然 1 になってはいけない、という定義もありえます）、どちらの定義かは言明を読まないと分かりません。
• 「区間演算の丸めが正しい向きである」は、言明ではなく証明の中身です。もし mulI が内向きに丸めていたら mulI_sound が証明できないので、そこで止まります。健全性の証明が通ったことが、丸めの向きの保証になっています。
• 証明書の探し方については何も言っていません。外の計算が別の木を出しても、検査が通れば同じ定理が出ます。

二つめが、この題材でいちばん読み違えやすいところです。定義に書いていない制約は、課されていません。続きは 通っても、言いたいことが言えているかへ。

出典と再現

次は 08 通っても、言いたいことが言えているか——このページの §08 と §09 を、手順として一般に書いたものです。用語は 12 用語集。