# 証明支援系 Lean の仕組み：カーネル・定義的同値・tactic・三つの公理 > Lean 4 が証明を確認する仕組みを、カーネルの型検査と定義的同値（β・δ・ι・ζ・η）、エラボレーションと単一化、tactic が項を作る過程に分けて説明する。公理 Quot.sound から関数外延性を、選択公理からディアコネスクの定理で排中律を証明し、de Bruijn 基準で信頼の境界を定める。 > https://rikai.mugen-giken.com/mathematics/logic-and-type-theory/lean-kernel ## 0. この記事の要点 コンピュータに数学の証明を確認させるソフトウェアがあります。そのソフトが「正しい」と言ったとき、私たちは何を信じていることになるのでしょうか。この記事は、Lean というソフトの内部を「証明を最終的に検査する小さな部分」と「それ以外」に分けて、信じる必要があるものを絞り込みます。読み終えると、Lean が受理した証明のどこまでを信頼でき、何は自分で確かめる必要があるのかを説明できるようになります。 - Lean で書いた証明は、**エラボレータ**（省略だらけのコードを、省略のない形に直す部分。記法の解釈・暗黙の引数の推論・tactic の実行）が依存型理論の項に翻訳し、**カーネル**がその項の型を検査します。正しさの判定に責任を負うのはカーネルだけで、エラボレータや tactic に誤りがあっても、誤った証明はカーネルで拒否されます。 - カーネルの仕事の中心は**定義的同値**の判定です。β（関数適用）・δ（定義の展開）・ι（帰納型の再帰子の計算）・ζ（`let` の展開）・η（関数の外延的な形）の簡約と、証明の無関係性（同じ命題の二つの証明は区別しないという約束）で一致する二つの項を同じとみなします。`rfl` が通るかどうかはこれで決まります。 - **tactic** は項を直接書く代わりに「穴（メタ変数。まだ決まっていない部分の仮置き）の空いた項」を少しずつ埋める道具です。`#print` で見れば、tactic 証明もただの λ 項です。 - Lean の標準の公理は `propext`・`Quot.sound`・`Classical.choice` の三つだけです。`Quot.sound` から**関数外延性**が（）、三つすべてから**排中律**が（ディアコネスクの定理、）、それぞれ定理として証明されます。どの定理がどの公理に依存するかは `#print axioms` で確かめられます。 - **de Bruijn 基準**：証明の正しさを、小さく独立に再実装できる検査器だけに依存させる、という設計原理です。Lean で「信頼しなければならないもの」と「信頼しなくてよいもの」の境界を整理します。 ## 1. 動機：計算機が「正しい」と言うとき、何を信じているのか ### 1.1. 計算機が確認した定理 この 20 年ほどで、人間の査読だけでは確信しきれない証明が、証明支援系で確認されるようになりました。四色定理は Coq で（ゴンティエ、2005 年）、ケプラー予想の証明は HOL Light と Isabelle で（Flyspeck プロジェクト、2014 年）、ショルツェの凝縮数学の中心定理は Lean で（Liquid Tensor Experiment、2022 年）形式化されました。現在、Lean の数学ライブラリ Mathlib には数十万の定理が収められています。 ここで素朴な疑問が湧きます。**その証明支援系自体が正しいと、なぜ言えるのか。** Lean は数十万行のプログラムで、自動証明の機能（`simp` など）は複雑です。プログラムにはバグがあるものです。「Lean が受理した」ことを「証明が正しい」ことの根拠にしてよいのでしょうか。 ### 1.2. 答えの骨格 この記事の答えは次のとおりです。 1. Lean の証明は最終的に、前章の依存型理論（CIC）の**項**になる。 2. その項が主張の型をもつかを判定するのは**カーネル**という小さな部分だけで、ほかの部分（数十万行の大部分）はカーネルに渡す項を作るための道具にすぎない。 3. カーネルが使う規則と公理は数えるほどしかなく、紙の上で書き下せる。その体系の無矛盾性は（集合論の強い公理を仮定すれば）証明されている。 4. だから信頼すべきものは「小さなカーネルの実装」と「三つの公理」と「主張の書き方」に絞られる。カーネルは独立に再実装でき、実際に別の検査器で同じ証明を検査し直すことができる。 [計算可能性](/mathematics/logic-and-type-theory/computability) で見たように、証明を**見つける**ことは一般にアルゴリズムではできません。しかし証明を**検査する**ことはできます。Lean はこの非対称性を設計に取り込み、難しい「発見」を信頼しなくてよい部分に、易しい「検査」を信頼する部分に割り振っているのです。
ソース theorem … := by … エラボレータ 記法・暗黙の引数・単一化 型クラス・tactic（simp など） 数十万行・信頼不要 カーネル 型検査・定義的同値 環境 定理として登録 項 ＋ 公理 propext・Quot.sound・Classical.choice 独立な検査器で再検査できる
以下、この記事のコードはすべて Lean 4（4.34 系、標準ライブラリのみ）で動作を確認したものです。表示される文言は版によって多少変わることがあります。 ## 2. カーネルの型理論 ### 2.1. 項と宇宙 カーネルが扱う項（`Expr`）は、前章の [依存型理論](/mathematics/logic-and-type-theory/dependent-type-theory) の項とほぼ同じで、次の種類しかありません：束縛変数、[宇宙](/mathematics/logic-and-type-theory/dependent-type-theory#def-universe) `Sort u`、定数（定義済みの名前）、適用 `f a`、λ 抽象 `fun x : A => b`、[Π 型](/mathematics/logic-and-type-theory/dependent-type-theory#def-pi) `(x : A) → B`、`let x : A := v; b`、数と文字列のリテラル、構造体の射影。証明も、命題も、自然数も、関数も、すべてこの形の項です。 文脈 $\Gamma$ と環境（登録済みの定数と、その型・定義）のもとで、 1. $\Gamma\vdash\mathsf{Sort}\ u:\mathsf{Sort}\ (u+1)$。 2. $\Gamma\vdash A:\mathsf{Sort}\ u$ かつ $\Gamma,x{:}A\vdash B:\mathsf{Sort}\ v$ ならば $\Gamma\vdash(x:A)\to B:\mathsf{Sort}\ (\mathrm{imax}\ u\ v)$。ここで $\mathrm{imax}\ u\ 0=0$、$v\ne0$ なら $\mathrm{imax}\ u\ v=\max(u,v)$。 3. $\Gamma,x{:}A\vdash b:B$ ならば $\Gamma\vdash(\mathsf{fun}\ x:A\Rightarrow b):(x:A)\to B$。 4. $\Gamma\vdash f:(x:A)\to B$、$\Gamma\vdash a:A'$、$\Gamma\vdash A\equiv A'$ ならば $\Gamma\vdash f\,a:B[x:=a]$。 5. 定数 $c$ は環境に登録された型をもつ（宇宙変数は具体化してよい）。 規則 2 の $\mathrm{imax}$ が、`Prop`（$=\mathsf{Sort}\ 0$）の非可述性（）を表しています。終域が `Prop` なら、Π 型全体も `Prop` に落ちます。規則 4 の $\Gamma\vdash A\equiv A'$ が**定義的同値**で、次節の主役です。 カーネルは、これらの規則を下から組み立てる**型推論**のアルゴリズムとして実装されています。項を受け取り、その型を計算し、宣言された型と定義的に同値かを確かめる。定理の宣言 `theorem t : P := e` がカーネルを通るとは、$e$ の推論された型が $P$ と定義的に同値だということです。 ### 2.2. 帰納型と商 カーネルは `inductive` 宣言を受け取ると、その型・構成子・**再帰子**（前章の除去規則。自然数なら `Nat.rec`）を生成し、構成子が「正の位置」（定義中の型が、構成子の引数の型の中で関数の矢印の左側に現れないこと）にしか現れないことなどの条件を検査します（条件を外すと矛盾が作れるためです）。商型 `Quot` も組み込みで、 - `Quot r : Sort u`（$r:\alpha\to\alpha\to\mathsf{Prop}$）、`Quot.mk r a : Quot r`、 - `Quot.lift f h : Quot r → β`（$h$ は $f$ が $r$ を保つことの証明）、計算規則 `Quot.lift f h (Quot.mk r a) ≡ f a`、 - `Quot.ind`（商の元についての帰納法） が規則として、`Quot.sound : r a b → Quot.mk r a = Quot.mk r b` が公理として与えられています。[関係と同値関係](/mathematics/foundations/equivalence-relations) の商集合の普遍性（）を、規則として書いたものです。 ## 3. 定義的同値 「二つの項を同じとみなす」とは、計算して同じ形になることです。次の定義に出る五つの簡約は、それぞれ、関数に値を代入する計算（β）、名前を定義で置き換える計算（δ）、帰納型の場合分けにあたる計算（ι）、`let` の展開（ζ）、関数を「引数を取って適用するだけの形」に書き直すこと（η）です。直後の例で一つずつ確かめられます。 カーネルの定義的同値 $\equiv$ は、次の簡約で互いに移り合うことを中心に生成される同値関係である。 - **β**：$(\mathsf{fun}\ x\Rightarrow b)\,a\equiv b[x:=a]$。 - **δ**：定義された定数をその定義で置き換える。 - **ι**：再帰子を構成子に適用したものを計算する（例：`Nat.rec z s (n+1) ≡ s n (Nat.rec z s n)`）。`Quot.lift` の計算規則もこれに含める。 - **ζ**：`let x := v; b` $\equiv b[x:=v]$。 - **η**：$f\equiv(\mathsf{fun}\ x\Rightarrow f\,x)$。構造体については、各射影から組み直したものともとの項を同一視する（構造体 η）。 - **証明の無関係性**：$P:\mathsf{Prop}$ のとき、$h_1,h_2:P$ はつねに $h_1\equiv h_2$。 次の 6 行は、それぞれの規則だけで `rfl`（反射律 `Eq.refl` の項）が通る例です。 ```lean def double (n : Nat) : Nat := n + n example : (fun x => x + 1) 2 = 3 := rfl -- β example : double 3 = 6 := rfl -- δ example : Nat.rec (motive := fun _ => Nat) 0 (fun _ r => r + 2) 3 = 6 := rfl -- ι example : (let x := 2; x * x) = 4 := rfl -- ζ example (f : Nat → Nat) : (fun x => f x) = f := rfl -- η example (p : Prop) (h₁ h₂ : p) : h₁ = h₂ := rfl -- 証明の無関係性 ``` `rfl : a = a` に対して目標 `x = y` を与えると、カーネルは `a = a` と `x = y` の定義的同値、つまり $x\equiv y$ を判定します。逆に、定義的に同値でない等式は `rfl` では証明できません。 ```lean example (n : Nat) : n + 0 = n := rfl -- 通る：加法は第 2 引数の再帰で定義されている example (n : Nat) : 0 + n = n := rfl -- エラー：n が変数なので ι 簡約が進まない ``` 1 行目は `n + 0` が加法の定義の `0` の場合に ι 簡約され、`n` になります。2 行目は、加法の再帰が第 2 引数 `n` で行われるのに `n` が変数なので、計算が止まってしまいます。前章で見た「$n+0\equiv n$ は計算、$0+n=n$ は帰納法」（）の区別が、そのまま現れています。 カーネルは二つの項を弱頭部正規形（先頭の簡約だけを進めた形）にしてから先頭を比べ、一致すれば引数を再帰的に比べます。δ 簡約はどちらの定義をいつ展開するかを発見的に選び（遅延 δ 簡約）、η と証明の無関係性は先頭が合わないときに試します。この判定はすべての場合に止まるとは限らず（巨大な計算を要求すれば事実上止まりません）、カルネイロ (M. Carneiro, 2019) は、Lean の理論における定義的同値が決定不能であり、カーネルの判定アルゴリズムは推移律を満たさない場合があること（ただし健全であること）を示しました。主張のみ述べます。実用上は「カーネルが同値と答えたものは、理論の上でも同値」という健全性だけが信頼に関わります。 ## 4. エラボレーションと単一化 人間が書くソースコードは、カーネルが読む項よりずっと省略されています。`2 + 2` の背後には型・型クラスのインスタンス・数リテラルの解釈が隠れています。 ```lean set_option pp.explicit true in #check (2 + 2 : Nat) -- @HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) -- (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) : Nat ``` この省略を埋めるのが**エラボレータ**です。主な仕事は三つあります。 - **暗黙の引数**：`{A : Type}` と宣言された引数は書かなくてよい。エラボレータは**メタ変数** `?A` を置き、後で埋める。 - **単一化**：型検査の途中で「`?A → ?A` と `Nat → Nat` が等しくなるように `?A` を決めよ」という問題が生じる。エラボレータはメタ変数への代入を探し、`?A := Nat` を見つける。高階の単一化は一般には決定不能なので、Lean は扱いやすい断片（パターン単一化）を中心に、発見的な手続きで解く。 - **型クラスの解決**：`+` は `HAdd` という型クラスのメソッドで、`Nat` の場合のインスタンス `instHAdd` を探索して埋める。 エラボレーションは**失敗してもよい**部分です。単一化が解けなければエラーを出すだけで、誤った項を作っても、カーネルがそれを拒否します。だからエラボレータは発見的な手続きを自由に使えます。 ## 5. tactic は項を作る `by` の後に書く tactic は、目標（型）を受け取り、**穴の空いた項**を少しずつ埋めていく命令です。各時点の「ゴール」は、まだ埋まっていないメタ変数とその型にほかなりません。 ```lean theorem pq (p q : Prop) (hp : p) (hq : q) : p ∧ q := by constructor · exact hp · exact hq #print pq -- theorem pq : ∀ (p q : Prop), p → q → p ∧ q := -- fun p q hp hq => ⟨hp, hq⟩ ``` 最初のゴールは `?m : p ∧ q` です。`constructor` は `And` の構成子 `And.intro` を当てはめて `?m := And.intro ?m₁ ?m₂` とし、新しいゴール `?m₁ : p`、`?m₂ : q` を作ります。`exact hp` は `?m₁ := hp` と埋めます。すべての穴が埋まると、項 `⟨hp, hq⟩`（`And.intro hp hq`）が完成し、カーネルに渡されます。 帰納法と書き換えを使う証明も同じです。 ```lean theorem zero_add' (n : Nat) : 0 + n = n := by induction n with | zero => rfl | succ k ih => rw [Nat.add_succ, ih] #print zero_add' -- fun n => Nat.recAux (Eq.refl (0 + 0)) -- (fun k ih => Eq.mpr (id (congrArg (fun _a => _a = k + 1) (Nat.add_succ 0 k))) -- (Eq.mpr (id (congrArg (fun _a => _a.succ = k + 1) ih)) (Eq.refl k.succ))) n ``` `induction` は再帰子（ここでは `Nat.recAux`、`Nat.rec` の使いやすい形）を当てはめ、`rw` は等式による書き換えを `Eq.mpr` と `congrArg`（前章の輸送と合同、）の組み合わせとして項に記録しています。`simp` のような強力な自動化も、最終的にはこうした項を出力します。tactic は「証明を見つける手伝い」であり、「証明が正しいことの根拠」ではありません。根拠は出力された項と、それを検査するカーネルです。 ## 6. 三つの公理 ### 6.1. 公理の一覧 CIC の規則だけでは、ふつうの数学で使う推論のいくつかが証明できません（前章の ）。Lean の標準ライブラリは、次の三つを公理として加えています。 ```lean #check @propext -- ∀ {a b : Prop}, (a ↔ b) → a = b #check @Quot.sound -- ∀ {α : Sort u_1} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r b #check @Classical.choice -- {α : Sort u_1} → Nonempty α → α ``` 1. **命題外延性** `propext`：同値な命題は等しい。 2. **商の健全性** `Quot.sound`：$r\,a\,b$ ならば、商 `Quot r` で $a$ と $b$ の類は等しい。 3. **大域選択** `Classical.choice`：型 $\alpha$ が空でない（`Nonempty α`。これは `Prop` に属する）ならば、$\alpha$ の元を一つ返す。 `Classical.choice` は、命題 `Nonempty α` の証明（中身を取り出せないもの。）から、**データ**としての元を取り出す公理です。前章で `∃` から証人を取り出せない理由を見ましたが、この公理はまさにその穴を、計算できない定数として埋めています。この公理を使って定義した関数には `noncomputable` という印が付き、実行できません。 ### 6.2. 関数外延性 ここでのねらいは、「すべての点で値が等しい関数は等しい」という、ふつうの数学では当たり前の事実が、公理 `Quot.sound` から導けることを見ることです。方針は、関数全体を「すべての点で値が等しい」という関係で割った商を作り、割った後で等しいことを、もとの関数の等しさに引き戻す、というものです。 `Quot.sound` のもとで、$f,g:(x:\alpha)\to\beta\,x$ がすべての $x$ で $f\,x=g\,x$ を満たすならば $f=g$。 関数の型の上の関係 $f\sim g:\iff\forall x,\ f\,x=g\,x$ をとり、商 $Q=\mathsf{Quot}\ {\sim}$ を作る。写像 $\mathrm{app}:Q\to(x:\alpha)\to\beta\,x$ を $$ \mathrm{app}(q)(x):=\mathsf{Quot.lift}\ (\lambda f.\,f\,x)\ h_x\ q $$ で定める。$h_x$ は「$f\sim g$ ならば $f\,x=g\,x$」という、$\lambda f.\,f\,x$ が $\sim$ を保つことの証明で、$\sim$ の定義そのものから得られる。 仮定より $f\sim g$ なので、`Quot.sound` から $\mathsf{Quot.mk}\,f=\mathsf{Quot.mk}\,g$。両辺に $\mathrm{app}$ を施すと（合同、 (4)） $$ \mathrm{app}(\mathsf{Quot.mk}\,f)=\mathrm{app}(\mathsf{Quot.mk}\,g). $$ 左辺は `Quot.lift` の計算規則（ι）により $\lambda x.\,f\,x$ に、さらに η により $f$ に定義的に等しい。右辺も同様に $g$。変換規則により、これは $f=g$ の証明である。 Lean のコードにすると次のようになります。証明の最後の `show` が「定義的に等しい型への読み替え」で、カーネルが ι と η を使って確かめる部分です。 ```lean theorem my_funext {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : ∀ x, f x = g x) : f = g := by let eqv : ((x : α) → β x) → ((x : α) → β x) → Prop := fun f g => ∀ x, f x = g x let extfunApp (q : Quot eqv) (x : α) : β x := Quot.liftOn q (fun f => f x) (fun _ _ h => h x) show extfunApp (Quot.mk eqv f) = extfunApp (Quot.mk eqv g) exact congrArg extfunApp (Quot.sound h) #print axioms my_funext -- 'my_funext' depends on axioms: [Quot.sound] ``` ### 6.3. ディアコネスクの定理：選択公理から排中律へ [単純型付きラムダ計算とカリー＝ハワード対応](/mathematics/logic-and-type-theory/simple-types-curry-howard) で見たように、排中律は構成的な論理には含まれません。ところが、[選択公理](/mathematics/foundations/axiom-of-choice-zorn#ax-choice)を加えると排中律が**証明できてしまいます**。 `propext`、関数外延性（）、`Classical.choice` のもとで、任意の命題 $p$ について $p\vee\neg p$。 証明の方針は次のとおりです。命題 $p$ の真偽を知らないまま、二つの述語 $U,V$ を「$p$ が真なら一致し、偽なら食い違う」ように作ります。そして、それぞれから選択関数で元を一つずつ選び、選ばれた二つが等しいかどうかを見ると、$p$ の真偽が決まる、という筋書きです。証明中の「輸送」は、等しい二つのものの一方についての主張を、他方についての主張へ移すことを指します。 $p$ を固定し、命題についての二つの述語を $$ U(x):\iff(x=\mathsf{True})\vee p,\qquad V(x):\iff(x=\mathsf{False})\vee p\qquad(x:\mathsf{Prop}) $$ とおく。$U(\mathsf{True})$ と $V(\mathsf{False})$ が成り立つので、$\exists x\,U(x)$ と $\exists x\,V(x)$ の証明 $e_U,e_V$ がある。`Classical.choice` から作られる選択関数 $\varepsilon$（述語 $P$ と $\exists x\,P(x)$ の証明を受け取り、$P$ を満たす元を返す）で $u:=\varepsilon(U,e_U)$、$v:=\varepsilon(V,e_V)$ とすると、$U(u)$ かつ $V(v)$。 **段階 1：$u\ne v$ または $p$。** $U(u)$ と $V(v)$ を場合分けする。どちらかで $p$ の側が成り立てば $p$。そうでなければ $u=\mathsf{True}$ かつ $v=\mathsf{False}$ で、$\mathsf{True}\ne\mathsf{False}$（$\mathsf{True}=\mathsf{False}$ なら輸送で $\mathsf{False}$ の証明が得られる）だから $u\ne v$。 **段階 2：$p$ ならば $u=v$。** $p$ を仮定すると、すべての $x$ で $U(x)$ と $V(x)$ はともに真なので $U(x)\leftrightarrow V(x)$。`propext` で $U(x)=V(x)$、関数外延性で $U=V$。$\varepsilon$ は関数なので、等しい入力には等しい出力を返す。ここで入力は述語と存在の証明の組だが、$U=V$ に沿って $e_U$ を輸送したものと $e_V$ は同じ命題 $\exists x\,V(x)$ の証明なので、証明の無関係性により等しい。よって $u=\varepsilon(U,e_U)=\varepsilon(V,e_V)=v$。 **結論。** 段階 1 で $p$ ならそれで終わり。$u\ne v$ なら、段階 2 の[対偶](/mathematics/foundations/proof-techniques#def-converse-contrapositive)から $\neg p$。いずれにせよ $p\vee\neg p$。 証明の核心は段階 2 で、**選択関数が述語の外延だけで値を決める**ことです。$p$ が真なら $U$ と $V$ は同じ述語になり、同じものが選ばれる。$p$ が偽なら $U=\{\mathsf{True}\}$、$V=\{\mathsf{False}\}$ で、違うものが選ばれる。つまり、選ばれた $u,v$ が等しいかどうかを見れば $p$ の真偽が分かってしまう、という仕組みです。
p が真のとき U(x) も V(x) もすべての x で成り立つ U = V（同じ述語） 選ばれる u と v は等しい p が偽のとき U は True だけ、V は False だけを満たす U と V は異なる述語 選ばれる u と v は異なる（True と False）
集合論の選択公理（）の場合にも、分出公理を使って同じ議論ができます（ディアコネスク 1975、グッドマンとマイヒル 1978）。 Lean の標準ライブラリの `Classical.em` は、この証明をそのまま形式化したものです。自分で書くと次のようになります。 ```lean theorem my_em (p : Prop) : p ∨ ¬p := by let U : Prop → Prop := fun x => x = True ∨ p let V : Prop → Prop := fun x => x = False ∨ p have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩ have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩ let u : Prop := Classical.choose exU let v : Prop := Classical.choose exV have u_def : U u := Classical.choose_spec exU have v_def : V v := Classical.choose_spec exV have not_uv_or_p : u ≠ v ∨ p := by cases u_def with | inr h => exact Or.inr h | inl hu => cases v_def with | inr h => exact Or.inr h | inl hv => exact Or.inl (by rw [hu, hv]; exact true_ne_false) have p_implies_uv : p → u = v := by intro hp have hpred : U = V := by funext x exact propext ⟨fun _ => Or.inr hp, fun _ => Or.inr hp⟩ have h₀ : ∀ (eU : ∃ x, U x) (eV : ∃ x, V x), Classical.choose eU = Classical.choose eV := by rw [hpred] intro eU eV rfl exact h₀ exU exV cases not_uv_or_p with | inl hne => exact Or.inr (fun hp => hne (p_implies_uv hp)) | inr h => exact Or.inl h #print axioms my_em -- 'my_em' depends on axioms: [propext, Classical.choice, Quot.sound] ``` `h₀` の証明で、`rw [hpred]` が $V$ を $U$ に書き換えた後、`rfl` が通るのは証明の無関係性のためです（`Classical.choose eU` と `Classical.choose eV` は、証明 `eU` と `eV` が定義的に等しいので定義的に等しい）。`funext` は標準ライブラリの関数外延性で、`Quot.sound` に依存するため、`#print axioms` には三つの公理すべてが現れます。 排中律があれば、背理法（二重否定の除去）、すべての命題の決定可能性（`Classical.propDecidable`）、`if p then … else …` を任意の命題 $p$ で書くことが可能になります。Mathlib の大部分の定理はこれらに依存しており、`#print axioms` を実行すると、ほとんどの場合三つの公理すべてが表示されます。「Lean の数学は古典数学である」というのは、この三つの公理を受け入れているという意味です。 ## 7. de Bruijn 基準と信頼の境界 証明支援系が **de Bruijn 基準**を満たすとは、それが生成する証明が、独立に書かれた十分小さな検査プログラムで検査できる形の**証明対象**として出力されることをいう。 この名前は、1960 年代に最初の証明支援系 AUTOMATH を作ったデ・ブラウンにちなみ、バレンドレフトとウィーディクが命名したものです。Lean はこの基準を満たします。カーネルに渡された項は書き出すことができ、それを別の実装の検査器（Rust で書かれた nanoda、Lean 自身で書き直された lean4lean など）で検査し直すことができます。Lean の配布物には、環境全体をカーネルで再検査するツール `leanchecker` も含まれています。 Lean で形式化された定理を信じるとき、信頼しているものを列挙すると次のようになります。 | 信頼しなければならないもの | 信頼しなくてよいもの | |---|---| | カーネルの実装（または独立な検査器のどれか） | パーサ、エラボレータ、単一化、型クラスの解決 | | 使った公理（`#print axioms` で列挙される） | tactic（`simp`、`omega`、`decide` など）の実装 | | **定義と主張が意図どおりに書かれていること** | Mathlib の自動化、外部の探索ツール、生成 AI による証明案 | | 体系そのものの無矛盾性 | 証明の長さや読みやすさ | `#print axioms` は境界を見張る道具でもあります。証明を `sorry` で済ませると `sorryAx` が、コンパイル済みのコードによる計算を信じる tactic `native_decide` を使うと補助の公理が、それぞれ表示されます。 ```lean theorem bad : 1 = 2 := by sorry #print axioms bad -- 'bad' depends on axioms: [sorryAx] theorem dc : 2 ^ 10 = 1024 := by decide #print axioms dc -- 'dc' does not depend on any axioms ``` 表の左下の「無矛盾性」については、カルネイロ (2019) が Lean の型理論のモデルを、ZFC に[到達不能基数](/mathematics/category-homological-algebra/categories-functors#def-inaccessible)を可算個加えた集合論の中で構成し、相対的な[無矛盾性](/mathematics/logic-and-type-theory/incompleteness-theorems#def-metaproperties)を示しています（主張のみ）。第二不完全性定理（）により、これ以上を Lean 自身の中で示すことはできません。結局、形式化された証明の信頼性は「紙の上の数学で ZFC（と少しの大きな基数）を信じる」ことに帰着します。[公理的集合論 ZFC](/mathematics/logic-and-type-theory/axiomatic-set-theory) で Rikai の閉包の終点に置いたものと、ほぼ同じ場所です。 表の左の 3 行目、**定義と主張が正しいか**は、どんな検査器も肩代わりしてくれません。主張が `1 = 1` に化けていれば、正しく証明されても何の意味もないからです。この問題は次章 [Lean による数学の形式化](/mathematics/logic-and-type-theory/formalizing-in-lean) で、Rikai の定理を実際に形式化しながら考えます。 ## 8. 演習 `example : (fun f => f 2) (fun x => x * 3) = 6 := rfl` は通る。カーネルが $(\lambda f.f\,2)(\lambda x.x\cdot3)\equiv6$ を確かめるのに使う簡約を順に挙げよ。 β で $(\lambda x.x\cdot3)\,2$、もう一度 β で $2\cdot3$。$\cdot$ は `HMul.hMul` を経由して `Nat.mul` に至るので、型クラスのインスタンスと定義の δ 展開を行い、`Nat.mul` の計算（再帰子の ι 簡約。実際のカーネルは自然数リテラルの乗算を GMP で直接計算する特別な規則をもつ）で $6$ になる。こうして両辺の正規形が一致する。 排中律 `Classical.em` と `propext` を使って、任意の $p:\mathsf{Prop}$ について $p=\mathsf{True}\vee p=\mathsf{False}$ を示せ。 排中律で場合分けする。$p$ が成り立つとき、$p\leftrightarrow\mathsf{True}$（右向きは自明、左向きは $p$ の証明を返す）なので `propext` で $p=\mathsf{True}$。$\neg p$ のとき、$p\leftrightarrow\mathsf{False}$（右向きは $\neg p$、左向きは $\mathsf{False}$ の除去）なので $p=\mathsf{False}$。Lean では次のように書け、実行して確認できます。 ```lean theorem prop_two (p : Prop) : p = True ∨ p = False := by cases Classical.em p with | inl hp => exact Or.inl (propext ⟨fun _ => trivial, fun _ => hp⟩) | inr hn => exact Or.inr (propext ⟨fun hp => hn hp, fun h => h.elim⟩) ``` `Prop` が二つの元しかもたない「真理値の型」になるのは、古典論理と命題外延性を合わせたときです。 の証明で、(1) `propext` と関数外延性はどこで使われたか、(2) 選択関数が「存在の証明」を入力に取るにもかかわらず $u=v$ が言えたのはなぜか、を説明せよ。 (1) 段階 2 で、各 $x$ について $U(x)\leftrightarrow V(x)$ から $U(x)=V(x)$ を得るのに `propext`、そこから述語として $U=V$ を得るのに関数外延性を使った。どちらかが欠けると、$U$ と $V$ が「外延的には同じだが等しいとは言えない」状況が残り、選択関数に同じ入力を与えたことにならない。(2) 選択関数の入力は (述語, その存在の証明) の組である。$U=V$ に沿って輸送すると、$e_U$ は $\exists x\,V(x)$ の証明になり、$e_V$ と同じ命題の証明になる。Lean の `Prop` では証明の無関係性によって同じ命題の二つの証明は定義的に等しいので、組全体が等しく、出力も等しい。Lean のコードでは、`rw [hpred]` の後の `rfl` がちょうどこの事実を使っている。 ## 参考文献 - L. de Moura and S. Ullrich, "The Lean 4 Theorem Prover and Programming Language", in *Automated Deduction – CADE 28*, Lecture Notes in Computer Science 12699, Springer, 2021, 625–635. - M. Carneiro, *The Type Theory of Lean*, Master's thesis, Carnegie Mellon University, 2019. - J. Avigad, L. de Moura, S. Kong and S. Ullrich, *Theorem Proving in Lean 4* — [オンライン版](https://lean-lang.org/theorem_proving_in_lean4/)（とくに「Axioms and Computation」の章）。 - R. Diaconescu, "Axiom of choice and complementation", *Proceedings of the American Mathematical Society* 51 (1975), 176–178. - H. Barendregt and F. Wiedijk, "The challenge of computer mathematics", *Philosophical Transactions of the Royal Society A* 363 (2005), 2351–2375.