Lean では現実的に厳しいもの — 量・述べ方・在庫

紙で書けている証明が、Lean に載らないことがあります。理由は三つに分かれ、どれに当たっているかで打つ手が違います。

量の問題は測れます。述べ方の問題は設計の問題です。在庫の問題は、自分で積むか、紙に残すかの判断です。三つとも「できない」ではなく「いま払える費用でできない」で、費用の桁が違います。

実演 — decide の費用は探索空間で決まる

decide は有限の場合を全部数え上げます。費用は場合の数そのものです。小さな例で測ります。頂点 Fin k のうち最初の 4 点が互いに隣接するグラフを取り（4 点が互いに隣接していれば 3 色では塗れません）、3 色の塗り方が一つも無いことを decide に確かめさせます。塗り方は 3^k 通りです。

def Adj (k : ℕ) (i j : Fin k) : Bool := i.val < 4 && j.val < 4 && i.val ≠ j.val

def Proper (k : ℕ) (f : Fin k → Fin 3) : Bool :=
  decide (∀ i j : Fin k, Adj k i j = true → f i ≠ f j)

set_option maxRecDepth 100000 in
theorem noCol6 : ∀ f : Fin 6 → Fin 3, Proper 6 f = false := by decide

k を替えて検査の時間を測りました。import Mathlib だけのファイルが 5.01 秒なので、その差が decide の費用です。

読めることが三つあります。

• 費用は場合の数にほぼ比例します。81 通りで 0.4 秒、729 通りで 4.2 秒——9 倍で約 10 倍です
• 既定の設定で通る範囲は狭い。729 通りで既に再帰の深さの上限を超えます。set_option maxRecDepth で上げれば通ります
• 上げても次の上限が来る。6,561 通りでは heartbeat（決定的な計算量の上限）に当たります。ここを外すと止まらなくなります

この形の壁に当たったときにやることは、上限を上げて待つことではなく、1 件あたりの費用を測って全体の桁を出すことです。

実例 — 148 万件の判定は 100〜1000 CPU 時間

単位距離グラフの上界の議論では、候補のグラフを段階的に篩に掛けて落とします。篩の最初の段は、辺の集合だけを見て「点の数が多すぎる」「次数が大きすぎる」で落とす判定で、候補の 86% がここで落ちます。この判定を Lean の中で回すとどうなるかを測りました。

次の段はもっと重く、全体では 10²〜10³ CPU 時間の桁になります。証明書の本数（771 本）は既に手の内にある規模で、桁を支配しているのは判定を回す回数の側です。

この見積りから出る設計の話が一つあります。候補ごとに decide を打つのは、候補の個数が Lean の外で決まっているからです。候補の一覧を Lean の項として持ち込めば、decide の回数は 1 回になります。ただし一覧を項として持つと項の大きさが 10⁶ の桁になり、費用が「回数」から「項の大きさ」に移るだけかもしれません。どちらが安いかは測れる問いです。

存在は安く、非存在は高い

費用の非対称が一つあり、これは量の問題の中でいちばん効きます。

上の実演と同じ設定で、塗れる側を測ります。最初の 3 点だけが互いに隣接するグラフなら 3 色で塗れます。塗り方を一つ書いて渡します。

theorem col20 : ∃ f : Fin 20 → Fin 3, Proper3 20 f = true :=
  ⟨fun i => ⟨i.val % 3, Nat.mod_lt _ (by norm_num)⟩, by decide⟩

20 点でも 5.21 秒——基準との差は 0.2 秒です。探索空間は 3^20 = 34 億通りありますが、証人を渡せば数え上げは起きません。6 点の非存在（729 通り）より安く済みます。

だから篩の段を設計するときは、その段が「どちらの向き」に使われるかを先に見ます。篩は候補を落とす道具なので、どの段も非存在の向きに使われます。「3 色に塗れないから落とす」は、そのまま書くと網羅になります。

実例で言うと、上の篩の段のうち彩色を根拠にする印だけは Lean で回せません。15 点・3 色で 3^15 = 1,434 万通りの網羅になり、再帰の深さの上限で落ちます（実測）。言明そのものは初等的で、格子の上なら十行で閉じます。重さの出所は言明の難しさではなく、使う向きです。

この段を篩から外しても全体は閉じますが、下流に流れる候補が 4.8 倍に増えます。一つの段を落としたら下流の個数が何倍になるかを、見積りの中に変数として持っておきます。

候補を並べて一つずつ潰す形の議論には、二つの部分があります。

(ii) が難しいのは、量の問題ではありません。言明を立てる形が決まっていないのです。書くには少なくとも次が要ります。

• 「候補」の全体を Lean の型として持つこと。「11 点で独立数 3 以下のグラフ」の全体を、同型で割った形で型にする
• 同型の定義を Lean の中に置くこと。外の探索は同型なものを一つにまとめて数えている。その「まとめ方」を Lean の中で述べる
• 探索そのものの正しさ。枝刈りを含む探索が、捨てた枝に候補を残していないこと

三つ目が本体です。外の探索は速さのために枝を刈っていて、刈った理由は探索のコードの中にしかありません。それを Lean に移すのは、探索を Lean で書き直すのと同じ作業です。07 証明書を Lean に検査させるの分業（探すのは外・確かめるのは Lean）が、ここでは効きません。証明書に当たるものが無いからです。

Lean に入っているのは一覧の長さだけです。

theorem cands_card : cands.length = 117 := by decide

これは「一覧が 117 個ある」であって「候補が 117 個で全部」ではありません。両者の差は 08 通っても、言いたいことが言えているかの型②です。

だから等級を分けて書きます。(i) は Lean、(ii) は 計算 です。上界の主張は (i) と (ii) の両方に乗っているので、主張全体の等級は 計算 になります。定理名が付いているのは (i) だけなので、表を作らないとこの一段が落ちます。

三つ目は、下敷きになる数学がまだ形式化されていない場合です。この場合、費用は「自分で積む」費用になります。

在庫の有無は grep で分かります。mathlib のソースを検索した結果です。

この表が、何を紙に残すかを決めます。四つ目と五つ目のように部分的に在庫がある場合は、在る部分に繋ぐのが安いことがあります。球面の測度は在ったので、性質で定義した測度が mathlib の定義と一致することを示す定理を一本置いて繋げました（08 §04 の (c)）。

紙に残すと決める基準

次の三つが揃ったら、紙に残す判断です。

逆に、次のどれかに当たるなら紙に残しません。自分の議論の新しい部分である（引いてくるものではない）／在庫の一部を使えば繋がる／量の問題であって述べ方の問題ではない。

残したことを明記する書き方

紙に残した部分は、結果の表の中に行として置きます。書くのは三つです。

三つ目が効きます。継ぎ目の場所を書くと、読み手はそこだけを検分できます。「一部は紙です」とだけ書くと、どこを見ればよいか分かりません。

そして、紙の行が結論の直前にあるなら、結論の等級は紙です。Lean の行がいくつ並んでいても変わりません。受け取る側がこれを確かめる手順が 09 言明を読む手順の⑦にあります。

三つとも、結論は「Lean に載らない」ではなく「この部分は別の等級である」です。等級を分けて書けば、結果は使えます。分けずに書くと、Lean の行が紙の行を保証しているように読めてしまいます。

次は 11 よくある罠——上の上限に当たったときの文面と、その読み方です。用語は 12 用語集。