Lean とは何か — 証明を機械が検査するとはどういうことか

紙の上の証明は、人が読んで納得することで成り立ちます。Lean は別の形をとります。命題をひとつの型として書き、証明をその型を持つ項として書く。そして「この項は本当にこの型を持つか」を機械が調べる。型が合えば証明が通り、合わなければ通りません。

いちばん小さい例です。

theorem two_add_two : 2 + 2 = 4 := rfl

theorem の直後が名前、: の後が命題（型）、:= の後が証明（項）です。rfl は「両辺を定義に従って計算すると同じものになる」ことを主張する項です。2 + 2 は自然数の加法の定義に従って 4 まで計算でき、両辺が一致するので、これで閉じます。

同じ命題に、別の証明を付けることもできます。

theorem two_add_two_decide : 2 + 2 = 4 := by decide

theorem two_add_two_norm : 2 + 2 = 4 := by norm_num

by の後に書くものは tactic——証明の項を代わりに組み立てるプログラムです。decide は「真偽を有限手続きで決められる命題」を計算で閉じ、norm_num は数式の正規形を計算して閉じます。三つの定理は同じ命題を述べていて、どれも検査を通ります。

変数を含む命題も同じ形です。

example (a b : ℕ) : a + b = b + a := Nat.add_comm a b

example は名前を付けず検査だけさせる書き方です。ℕ は自然数の型、(a b : ℕ) は「型 ℕ の項 a, b を受け取る」という宣言です。Nat.add_comm は加法の交換法則で、a と b を渡すと a + b = b + a という型の項になります。補題を使うことが、関数に引数を渡すことと同じ形をしている——これが「証明が項である」ということの手触りです。

Lean には二層あります。

この二層の関係が、機械検査の信頼が置ける所を決めています。tactic が作った項は、最後に必ず kernel が検査します。kernel は tactic の中身を見ませんし、信じません。届いた項が型を持つかどうかだけを見る。

結果として二つのことが言えます。tactic に誤りがあっても、通った証明が誤りになるとは限りません——誤った項を作れば kernel が弾くからです。逆に、tactic が失敗しても、命題が偽であることにはなりません。ただ、その道具ではその項を組み立てられなかった、というだけです。

信頼しなければならないものは、kernel の実装と、次に見る公理、それに命題そのものの書き方に絞られます。この二層が Lean 全体のどこに位置し、kernel が項をどう読むかは 13 Lean の仕組み にあります。

Lean の論理には、証明せずに受け入れる命題——公理——が有限個あります。どの定理がどの公理に依拠しているかは、機械が答えます。

theorem and_true_self (p : Prop) : (p ∧ True) = p := by simp

theorem em_holds (p : Prop) : p ∨ ¬p := Classical.em p

theorem half_add_half : (1 : ℚ) / 2 + 1 / 2 = 1 := by norm_num

#print axioms and_true_self
#print axioms em_holds
#print axioms half_add_half

出力：

'and_true_self' depends on axioms: [propext]
'em_holds' depends on axioms: [propext, Classical.choice, Quot.sound]
'half_add_half' depends on axioms: [propext, Classical.choice, Quot.sound]

この三つが、Lean と mathlib の標準三公理です。

ここまでなら「よく使われている普通の数学」の範囲です。三つとも、古典論理と選択公理を使う通常の数学が暗黙に使っているものです。このサイトで Lean の札を付けている主張は、すべてこの三つ以下に収まっています（一覧は Lean 検証一式）。

同じ命題でも、証明の付け方で依拠する公理は変わります。最初の三つの定理を並べると：

'two_add_two' does not depend on any axioms
'two_add_two_decide' does not depend on any axioms
'two_add_two_norm' depends on axioms: [propext]

rfl と decide は計算だけで閉じるので公理を使いません。norm_num は途中で命題の書き換えを行うため propext が入ります。公理を使わない証明が、いちばん強い——そして「公理を使わない」ときの出力は上のように does not depend on any axioms という別の言い回しになります。公理の数を数える検査を書くなら、この言い回しも数えなければ取りこぼします。

証明を書きかけのまま先に進めたいとき、Lean には sorry という穴があります。書きかけの箇所に置くと、その部分を認めたことにして検査が進みます。

theorem every_even_is_sum_of_two_primes (n : ℕ) (hn : 4 ≤ n) (he : n % 2 = 0) :
    ∃ p q : ℕ, p.Prime ∧ q.Prime ∧ p + q = n := by
  sorry

#print axioms every_even_is_sum_of_two_primes

出力（警告にはファイル名と位置が付きます）：

warning: declaration uses `sorry`
'every_even_is_sum_of_two_primes' depends on axioms: [propext, sorryAx]

これは未解決問題です。それでも「検査は通ります」——sorry は sorryAx という公理を立て、その公理はあらゆる命題を証明してしまうからです。sorryAx が出た定理は何も言っていません。

穴は二つの形で見えます。検査中の警告 declaration uses `sorry` と、#print axioms の sorryAx。前者は警告なので、エラーだけを見ていると見落とします。後者は定理ごとに確実に出ます。だから外に出す主張の確かめには、警告ではなく #print axioms のほうを使います。

decide は判定手続きを kernel に走らせます。kernel の計算は遅く、対象が大きくなると止まります。

theorem sum_to_199 : (List.range 200).sum = 19900 := by decide

error: maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information

そこで native_decide という tactic があります。命題の判定を機械語にコンパイルして走らせ、その結果を公理として受け入れます。速い代わりに、何が起きるかは #print axioms にはっきり出ます。

theorem sum_to_19 : (List.range 20).sum = 190 := by decide

theorem sum_to_199 : (List.range 200).sum = 19900 := by native_decide

#print axioms sum_to_19
#print axioms sum_to_199

'sum_to_19' depends on axioms: [propext]
'sum_to_199' depends on axioms: [propext, sum_to_199._native.native_decide.ax_1_1]

見慣れない名前が増えています。中身を見ると：

#print sum_to_199._native.native_decide.ax_1_1

axiom sum_to_199._native.native_decide.ax_1_1 : decide ((List.range 200).sum = 19900) = true

「この判定の結果は true である」という公理が、この定理のために新しく立ちます。kernel は計算をやり直しません。つまり信頼の範囲が、kernel と標準三公理からコンパイラと実行環境まで広がります。数え上げの誤りやコンパイラの不具合が、そのまま定理の誤りになります。

これがこのサイトで native_decide を使わない理由です。Lean の札は、この公理が出ていないことも条件にしています。

#check @Lean.ofReduceBool

warning: `Lean.ofReduceBool` has been deprecated: in-kernel native reduction is
deprecated; assert native evaluations with axioms instead
Lean.ofReduceBool : ∀ (a b : Bool), Lean.reduceBool a = b → a = b

機械検査の結果を受け取ったとき、どこまでが機械の言い分で、どこからが人の言い分か。その境目です。

言いたかったことであること

命題は人が書きます。定義を弱くとる・量化の順を入れ替える・仮定をひとつ足す。どれも検査は通り、そして言明は別のものになります。「辺があれば距離が 1」と「辺があることと距離が 1 であることが同値」は違う命題で、前者で証明できることは後者で証明できることより少ない。この形の食い違いの実例は 08 にあります。

定義が意図どおりであること

短い例で見ます。素数の定義から「2 以上」の条件を落とすと、こうなります。

def NoSmallDivisor (n : ℕ) : Prop := ∀ d : ℕ, d ∣ n → d = 1 ∨ d = n

theorem one_has_no_small_divisor : NoSmallDivisor 1 := by
  intro d hd
  left
  exact Nat.dvd_one.mp hd

通ります。NoSmallDivisor 1 は真です。一方で：

theorem one_is_not_prime : ¬ Nat.Prime 1 := by decide

これも通ります。二つは矛盾していません——NoSmallDivisor は素数の定義ではないからです。Lean は、落とした条件を教えません。定義が意図と合っているかどうかを確かめるのは、書いた人と読む人の仕事です。

言明の外で行った計算

「候補を 117 類に絞り、その 117 類が条件を満たさないことを Lean で証明した」という結果があるとき、Lean が保証するのは後半だけです。候補が 117 類で尽くされていることは、別の計算で確かめたことであって、定理の中には入っていません。この区別を保つ書き方と読み方が 09 に、絞り込みそのものを Lean に入れられない理由が 10 にあります。

だからこのサイトの Lean の札には、必ず定理名を添えています。名前を辿れば言明が読め、言明を読めば、保証の範囲がどこで終わるかが分かります。

出典と再現

次は 02 使い方の入口——上のコード片を自分の手元で検査するところまで。用語は 12 用語集。