言明を読む手順 — 「Lean で検査済み」を受け取ったら

「Lean で検査した」と言われた結果を受け取ったとき、確かめられることは七つあります。前の四つは機械にやらせるもので、数分で終わります。後の三つは読むもので、こちらが本体です。

順序に意味があります。前半で「証明が本当に閉じているか」を見て、後半で「閉じている言明が、聞きたかった問題か」を見ます。前半が通っても後半が通らないことは普通に起こり、その型は 08 に四つ挙げました。

配布物を展開して、自分の機械で検査を通します。Lean 検証一式には verify.sh が付いていて、機械の RAM と CPU の数から並列数を決め、lake exe cache get と全体のビルドを一手で走らせ、最後に公理の一覧と穴の数を要約します。展開してその一本を叩くだけです。

個別のファイルだけを見たいときは、他のファイルに依存しない一本もの（連結版）を lake env lean に直接渡すのが速いです。連結版は import Mathlib の一行しか読まないので、その一本だけで閉じていることが分かります。

$ time lake env lean PerfectFamily.lean
'PerfectFamily.cube3_bool' does not depend on any axioms
'PerfectFamily.dir_count' depends on axioms: [propext, Quot.sound]
   ...（以下 22 行、③ で見る `#print axioms` の出力）
real	0m7.367s
$ echo $?
0

見るのは終了コードだけではありません。Lean はエラーが無くても警告を出すことがあり、警告の中には後の項で問題になるもの（sorry の使用・非推奨の名前）が混ざります。エラーも警告も一行も無いことを確かめます。上の実行で出ているのは #print axioms の出力だけで、エラーと警告は 0 行、終了コードは 0 でした。

検査が通らない場合、まず環境を疑います。Lean と mathlib の版が配布物の lean-toolchain と lake-manifest.json で固定されているので、版が合っていれば結果は一致します。版のずれで落ちる形は 11 よくある罠の最後にまとめました。

Lean には「証明を後回しにする」書き方があり、それを使った定理も検査は通ります。ソース全体を機械的に探します。

grep -rn -E 'sorry|admit|native_decide|nativeDecide|ofReduceBool' .

sorry を使った定理は、警告としても出ます。試しに一本置いて検査すると、こう出ます。

warning: declaration uses `sorry`

この警告は一行だけで、長い出力の中では見落とします。②の grep と④の公理の確認は、同じことを別の側から見るためにあります。

#print axioms 定理名 は、その定理が最終的に何に依拠しているかを並べます。依存の木を全部たどった結果なので、途中のどこかに穴があれば必ず出ます。

#print axioms PerfectFamily.no_perfectZ_of_five

出力はこうなります。

'PerfectFamily.no_perfectZ_of_five' depends on axioms: [propext, Quot.sound]

読み方の基準は一つです。

公理の欄がきれいであることは、言明が意味のあることを何も保証しません。偽の仮定を置いた定理も、空集合の上の全称も、標準三公理の内側で通ります（08 §04 に実物）。この項は「証明が閉じているか」だけを見ています。

看板になる定理が複数あるときは、#print axioms を並べただけのファイルを一本作っておくと、検査のたびに全部の公理が出ます。配布物では ChkAll.lean がその役です。

ここから本体です。定理名を読まずに、言明を読みます。そして言明に出てくる定義を一つずつ開いて、紙の側の定義と突き合わせます。

例として、超立方体の辺の族についての定理を取ります。言明はこうです。

theorem no_perfectZ_of_five {d : ℕ} (hd : 5 ≤ d) (J : Fin d → W d → Bool) : ¬ PerfectZ J

読めるのは「d ≥ 5 なら PerfectZ を満たす J は無い」までです。PerfectZ が何かを知らなければ、この定理は何も言っていません。開きます。

/--
`J μ x`：`x` から `x + e_μ` へ向かう辺が族に入る。

`PerfectZ J`：どのプラケット `(μ, ν, x)`（`μ ≠ ν`）についても、その 4 辺
`(μ, x)`・`(μ, x+e_ν)`・`(ν, x)`・`(ν, x+e_μ)` のうちちょうど一本が `J` に入る。
-/
def PerfectZ (J : Fin d → W d → Bool) : Prop :=
  ∀ μ ν : Fin d, μ ≠ ν → ∀ x : W d,
    (J μ x).toNat + (J μ (shift x ν)).toNat
      + (J ν x).toNat + (J ν (shift x μ)).toNat = 1

ここで突き合わせるのは「プラケットの 4 辺」が紙と同じ 4 辺かです。四つの項を一つずつ見ます。shift x ν はまだ開いていない定義なので、これも開きます。

def shift (x : W d) (i : Fin d) : W d := Function.update x i (x i + 1)

x の i 座標だけを 1 増やす関数です。したがって四つの項は、x から出る μ 方向の辺・x + e_ν から出る μ 方向の辺・x から出る ν 方向の辺・x + e_μ から出る ν 方向の辺で、これは平面 (μ, ν) の正方形の 4 辺です。紙の定義と一致します。

さらに W d の中身も見ます。

/-- `ℤ^d` の頂点。 -/
abbrev W (d : ℕ) : Type := Fin d → ℤ

無限格子です。周期を課していないので、定理は周期的でない族も含みます。これは言明の強さに直結する一点で、型を見ないと分かりません。同じ「完全な族」を周期格子 Fin d → ZMod L の上で述べた定理が別にあり、そちらとこちらは別の定理です。

この一続きが手順です。

この手順を踏むと、08 §02 の「同じ言葉の下に二つの定義が並ぶ」型が見つかります。定義の名前が同じでも、開いた中身が違えば別の定理です。

言明の : の左側に並んでいるものが仮定です。一つずつ、誰が満たすのかを決めます。

三つ目が肝です。扱いにくい部分を仮定に追い出して残りを閉じるのは普通の進め方ですが、追い出した仮定を誰も満たしていないなら、結論はまだ使えません。08 §05 に、同じ結論を述べる三段の定理で仮定が消えていく実例があります。

見分け方は一つです。その仮定を満たす具体例が、同じ配布物の中に定理として在るか。在れば追い出しは解消されており、無ければ解消されていません。

decide で「成り立つ」を出した判定は、判定が何でも通しているだけかもしれません。これを排除するのが対照です。

陰性対照は、正解を一箇所だけ壊したものが入っているかを見ます。空のものと満杯のものが落ちるだけでは、判定が粗くても通ります。実物は 08 §04 の (b) にあります。

対照が一本も無い場合、それは結果が誤りだという意味ではありませんが、受け取る側が自分で対照を書いて確かめることになります。判定関数に極端な入力を入れて decide を回すだけなので、数行で済みます。

ひとまとまりの結果には、各行がどの等級かを書いた表が付いているべきです。表が無いときは、次の三つが混ざったまま渡されています。

Lean機械検査済み。定理名が添えてあることを見ます。名前が無い行は、確かめる手段がありません。 紙証明はあるが機械検査は未了。どこまでが紙かが書いてあることを見ます。 計算手元の計算で確かめた範囲。外に出す主張にしていないことを見ます。

表を見るときの要点は、Lean の行と紙の行の継ぎ目を探すことです。継ぎ目が結論の直前にあるなら、結論は紙の等級です。08 §06 に二つの例があり、どちらも継ぎ目が一箇所に見えるように書いてあります。

もう一つ、「列挙がそれで全部」の行が表に在るかを見ます。候補を並べて一つずつ潰す形の結果では、並べた候補が全部であることが別の等級になります。この行は抜けやすく、抜けると上界が丸ごと機械検査済みに見えます（10 §03）。

1〜4 が通り 5〜8 のどこかが通らない、というのが最も多い形です。そのとき結果は誤りではなく、言明が思っていたものと違います。違いの型は 08 の四つに当てはまります。

次は 10 Lean では現実的に厳しいもの——受け取る側が「なぜこの行は紙のままなのか」を読むための背景です。用語は 12 用語集。