- Leanには「依存型」という仕組みがあり、値や式を埋め込んだ複雑な型を定義できます。
- この複雑な型を作って、その型を持つ値を定義したコードが型チェックを通るか、コンパイルします。
- というのも、型と証明を対応させて考えるやり方（Curry–Howard同型）があり、その型の式が型チェックを通るなら、「型に対応した証明が成り立つ」ことが検証できたことになるのです。
import Mathlib.Data.Nat.GCD.Basic
import Mathlib.Data.Nat.Fib.Basic
-- フィボナッチ数列の隣接する2項の最大公約数は1
lemma fib_gcd (n : ℕ) : Nat.gcd (Nat.fib n) (Nat.fib (n + 1)) = 1 := by
induction n with
| zero =>
simp [Nat.fib]
| succ n ih =>
rw [Nat.fib_add_two]
rw [Nat.gcd_comm]
rw [Nat.gcd_add_self_right]
exact ihCode language: Haskell (haskell)
とんでもなく長いけど、「fib_gcd (n : ℕ)」の型が「Nat.gcd (Nat.fib n) (Nat.fib (n + 1)) = 1」という等式全体で、変数の値に相当するのが「by induction ...」 のブロックです。
ちょっとHaskellっぽい見た目だね。
C言語の「char ch = 'a'; 」みたいな変数定義からすると、ずいぶん遠いに来たなー。
1. Leanコンパイラと証明
Lean は、「数学的な証明を検証できる関数型プログラミング言語」です。
とはいえ、一般のプログラミング言語とどのような関係にあるのかイメージしにくいです。
そこで、Lean を型検査の計算が強いプログラミング言語として、その仕組みを見てみたいと思います1。
Leanは、コンパイラ前段の能力である型検査（型チェック）を拡張した結果として、命題の検査もできるようになっています2。
Lean のコンパイラが行う処理は、最初のステップは一般的なコンパイラとほぼ同じです。
ソースコード
↓
字句解析・構文解析 ← ここは C も Lean も同じ
↓
名前解決・スコープ確定
↓
型推論・型検査 ← Lean はここで計算が走る（依存型）
↓
コード生成・最適化字句解析と構文解析でソースを構文木（AST）に変換し、名前解決でスコープを確定します。
型情報のない式は、型推論で型を割り当て、型検査で矛盾がないかを確かめます。
ここまでは ほかのプログラミング言語とコンパイラと概念的に連続しています。
違いは、型検査の段階でできることの幅です。
それは「依存型」という仕組みで、型の中にさまざまな計算が埋め込めます3。
ちなみに、証明支援システムは、Leanより以前にも、CoqやIsabelleのようにありました。
ところが、これらは証明を書くためだけの言語で、実際のプログラムと切り離されていて、「プログラムが正しいことを証明したい」というときに、プログラムと証明を別々に管理する必要がありました。Leanは、「プログラムそのものを証明の対象にできる」という設計で、関数型プログラムと証明が同じ型理論の上に乗っているのが特徴です。
1.1. 型が一致するか検査する（C言語の場合）
Leanの型検査を、よりシンプルなC言語のコンパイラと比較してみましょう。
C コンパイラの型検査の出発点は、シンボルテーブルを引いて「この式の型は何か」を決定する処理です。
変数や関数の型をテーブルに登録しておき、使われるたびに引いて照合します。
int add(int a, int b) {
return a + b;
}
int n = add(1, 2); // OK：add の戻り値は int
int *p = add(1, 2); // エラー：整数をポインタに変換できないCode language: Arduino (arduino)*pへの代入でエラーになるのは、このadd関数の戻り値の型と整合しないからです。
シンボルテーブル:
add → (int, int) → int
型検査:
add(1, 2) の型 ──→ int
n の型 int ──→ 一致 → OK
p の型 int* ──→ 変換規則なし → エラーちなみに、C言語では型の暗黙の変換が多くあります。
たとえば、整数と浮動小数点数など、同じように処理できるようになっています。
int i = 42;
double d = i; // 型検査で int とわかった上で double へ変換（値は 42.0）
int j = 3.14; // 型検査で double とわかった上で int へ変換（3 に切り捨て、警告）
double sqrt(double x);
sqrt(4); // 4 が int とわかった上で double に変換して渡すCode language: Arduino (arduino)このような暗黙の型変換が可能なのも、型を検査しているからです。
型検査は「型を調べて一致するか確かめる」処理で、型が一致しないとわかったとき、エラーにするだけでなく、たとえば、int を double に暗黙に変換すべきかどうか決めています。
1.2. 型の構造の整合性を検査すく（C言語の場合）
C コンパイラの型検査は、シンボルテーブルを引くだけではありません。
型を組み立てるときの構造的な整合性も確かめます。
C の型検査が行う構造的な計算:
ポインタ int** ──→ * を剥がす ──→ int* ──→ * を剥がす ──→ int
配列 int[] ──→ [] を剥がす ──→ int
struct Point ──→ .x を引く ──→ int
関数 引数列・戻り値の照合Code language: CSS (css)これは、「型の構造を分解して整合性を確かめる」処理で、型同士の演算とみなせます。
この考え方は、Leanにつながります。
ポインタ型では、* を剥がして指し先の型を取り出し、代入先と照合します。
int x = 10;
int *p = &x; // OK：int* に int* を代入
*p = 20; // *p の型は int → OK
char *q = &x; // エラー：int* を char* に代入できないCode language: Arduino (arduino)struct 型では、フィールド名でメンバの型を引き、アクセスの整合性を確かめます。
struct Point { int x; int y; };
struct Point pt = {1, 2};
pt.x = 5; // OK：x は int
pt.x = "hello"; // エラー：int に char* を代入できない
pt.z = 0; // エラー：z というフィールドは存在しないCode language: Arduino (arduino)配列型では、要素型を取り出してアクセスの型を決めます。
ただし、配列の長さ情報による境界検査はなく、未定義動作になります4。
int arr[5];
arr[2] = 10; // OK：arr[i] の型は int
arr[9] = 10; // コンパイルは通る。範囲外かどうかは型に含まれていないCode language: Arduino (arduino)関数型では、引数と戻り値の型が宣言と一致するかを確かめます。
int add(int a, int b) { return a + b; }
add(1, 2); // OK
add(1, 2.5); // OK：double → int の暗黙変換が入る
add(1, (int*)0); // エラー：ポインタを int に変換できないCode language: Arduino (arduino)この意味で C の型検査はすでに演算的です。
ただし、型に入れられる情報には限界があります。
配列の長さ、ポインタが指す先の有効性、整数の値域などは型の外にあり、コンパイラはそこまで知りません。
1.3. 計算を含む型検査（Lean の場合）
さて、ようやく Lean の型検査の話です。
Lean では、型に入れられる情報として、「いくつか」「どの値か」も含められます。
たとえば、Leanには Vector 型があります。
def v1 : Vector Int 3 := ⟨#[1, 2, 3], by decide⟩
def v2 : Vector Int 5 := ⟨#[1, 2, 3, 4, 5], by decide⟩Code language: PHP (php)Vector α n は「要素型 α、長さ n のベクタ」です。
型にも式を埋め込められ、型検査の中で計算が評価されます。
def v3 : Vector Int (2 + 3) := ⟨#[1, 2, 3, 4, 5], by decide⟩
def v4 : Vector Int 5 := ⟨#[1, 2, 3, 4, 5], by decide⟩
-- この二つは同じ型。
型検査器が 2 + 3 を評価して 5 と確かめるCode language: PHP (php)長さが型に入っているので、長さの合わない操作を実行時ではなくコンパイル時に弾けます。
Lean の型検査（Vec）:
def append (xs : Vector α m) (ys : Vector α n) : Vector α (m + n) :=
⟨xs.toArray ++ ys.toArray, by
simp [Vector.toArray]
⟩
要素型 Int も長さ 5 も型に入る
長さが合わない操作はコンパイルエラーになる
append : Vec α m → Vec α n → Vec α (m + n)
↑
型検査器が m + n を計算して
結果の長さを検証するC言語の配列では、値の型はチェックできても、数については対象外です5。
そのような検証では、別の静的解析ツールで検出する必要があります。
一方、Lean ではサイズのような値も「型の一部」として演算の対象に含められます。
この差が、後で述べる命題を証明することにつながります。
2. Leanのインストール（macOS）
さて、ちょっと Lean の雰囲気をつかんだところで、実行環境を用意してみます。
Lean のツールチェーン管理には elan を使います。
Rust の rustup に相当するもので、プロジェクトの lean-toolchain ファイルに記載されたバージョンを自動的に選択・ダウンロードします6。
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | shCode language: Bash (bash)インストール後、シェルを再起動するか source ~/.zshrc を実行します。elan と lake が使えるようになっていれば準備完了です。
elan --version # elan 3.x.x
lake --version # Lake x.x.xCode language: Bash (bash)lake は Lean のビルドシステムで、依存パッケージの管理も兼ねています。
プロジェクトの作成はこうします。
lake new hello
cd hello
lake buildCode language: Bash (bash)code --install-extension leanprover.lean4Code language: Bash (bash)2.1. 動かしてみる
まず関数を定義して呼び出します。hello/Main.lean をこう書きます。
def greet (name : String) : String :=
"Hello, " ++ name ++ "!"
#eval greet "Lean" -- "Hello, Lean!"Code language: PHP (php)#eval は式をその場で評価して結果を表示するコマンドです。
VS Code なら lean4 拡張を入れると、行の横にインラインで結果が出て、lake build を通さなくても即座に確認できます7。
2.2. Leanの型検査
次に、型検査がどう働くかを実際に見てみましょう。
def double (n : Nat) : Nat := n * 2
#eval double 5 -- 10
#eval double "x" -- エラー：String は Nat ではないCode language: PHP (php)double "x" はコンパイルエラーになります。String を Nat に渡そうとしていることを型検査器が弾きます。
この段階ではまだ普通の型検査ですが、この仕組みが後で依存型まで拡張されていきます。
3. 依存型と前提条件
関数型言語では、型と値が別の世界にあることが自然です。
たとえば、Int → Bool という型は、Int の値を受け取って Bool の値を返す関数を表します。
普通の型の世界:
型の層 ┃ Int Bool List Int
────╂──────────────────
値の層 ┃ 1 true [1,2,3]
型は値を知らない。
値が変わっても型は変わらない。Code language: PHP (php)しかし、「依存型」では、型の中に値が入ります8。
依存型の世界:
型の層 ┃ Vec Int 2 Vec Int 3 Vec Int n
────╂───────────────────────
値の層 ┃ [1, 2] [1, 2, 3] ...Code language: CSS (css)依存型では型の中に値 (2, 3, n) が入っていて、長さが違えば別の型として区別されます。
関数型やペア型にも依存型を作れます。
具体的に見てみます。
-- 普通の関数型
def isPositive : Int → Bool := fun n => n > 0
-- 依存関数型（Π型）：戻り値の型が引数 n の値に依存する
def replicate : (n : Nat) → Vec Int n :=
fun n => Vec.replicate n 0
-- ↑
-- n によって戻ってくる型が変わるCode language: PHP (php)「 (n : Nat) → Vec Int n」の部分が依存関数型です。
ペア型でも同じことが起きます。
-- 普通のペア型
def p : Int × Bool := (42, true)
-- 依存ペア型（Σ型）：「ある n が存在して、長さ n のベクタがある」
def q : Σ n : Nat, Vec Int n := ⟨3, [1, 2, 3]⟩
-- ↑ n の値によって、ペアの2要素目の型が決まるCode language: JavaScript (javascript)「Σ n : Nat, Vec Int n」が依存ペア型です。
3.1. assert から依存型へ
たとえば、配列を使ったコードで、こういう記述をしたことがあるはずです。
int get(int *arr, int len, int index) {
assert(index >= 0 && index < len); // 実行時に確認
return arr[index];
}Code language: Arduino (arduino)この assert は実行されるまで確認されません。
型にはインデックスの範囲が書かれていないので、コンパイラはこの不変条件を知りません。
C の配列アクセス:
コンパイル時 get(arr, 10, i)
↑
i の範囲は型からわからない
↓（実行時まで持ち越し）
実行時 assert(i >= 0 && i < 10)
├─ 失敗 → プロセス終了 / 未定義動作
└─ 成功 → arr[i] を返すCode language: JavaScript (javascript)ところが、依存型があれば、この不変条件の一部を型にコンパイル時に前倒しできます9。
def safeGet (xs : Vector α n) (i : Fin n) : α :=
xs.get iFin n は「0 以上 n 未満の自然数」を表す型で、範囲外の値はそもそも Fin n 型に属しません。
つまり、範囲情報を含んだ整数型 Fin n があり、その型の値であれば配列範囲内であることが自動的に満たされます。
Lean の依存型を使った配列アクセス:
コンパイル時 safeGet xs (i : Fin n)
↑
i が 0..n-1 の範囲内であることを
型が保証。範囲外は Fin n を構築できない
↓（実行時は何もしない）
実行時 xs.get i ← assert 不要Code language: CSS (css)もちろん、外部から入力された値は実行時まで値がわからないため、実行時検査は残ります。
def fromUserInput (idx : Nat) (xs : Vector α n) : Option α :=
if h : idx < n then
some (safeGet xs ⟨idx, h⟩)
else
noneCode language: JavaScript (javascript)4. なぜ依存型が命題証明に使えるのか
通常のプログラムでの型チェックのエラーは、型に合わない値を入れることです。
しかし、Lean には値（あるいは項）に対して、型そのものが合うかどうか検査することも多いです。
ここまでの話を振り返ると、Lean の型検査器は型の中に値が入った式を計算できることがわかりました。Vector Int (2 + 3) を Vector Int 5 と同じ型だと認識するのは、型検査の中で 2 + 3 を実際に計算しているからです。
つまり、複雑な型をシンプルに簡約できます。
この計算能力が、命題証明へのドアを開きます。
4.1. TypeとProp
C の型検査では int や double のような「形」だけが型でした。
しかし、Leanの型は、データを表す Type（IntやString、Bool、Vectorなどが属する）と、命題を表す Prop に分かれています。
たとえば、3は、Nat型の値ですが、IntやNat、VectorなどはTypeそのものです。
#check 3 -- Nat
#check Nat -- Type
#check Vector Int 3 -- TypeCode language: CSS (css)Vectorそのものは、型コンストラクタです。
#check Vector -- Type → Nat → TypeCode language: CSS (css)等式をもとに型を作る型コンストラクタは、Eqです。1 + 1 = 2 という等式は、型コンストラクタ Eq でProp 型の1つとして書けます。
#check Eq Nat (1 + 1) 2 -- Prop
#check Eq -- {α : Type u} → α → α → PropCode language: PHP (php)Eqは、中置記法で書けるので、
#check (1 + 1 = 2) -- PropCode language: PHP (php)のように書くと、Prop 型になります。
ちなみに、Type によって定義された変数は、実行時に値として存在します。
しかし、Prop は証明の世界で使われ、実行時には消去されます。
証明が存在するかどうかだけが重要で、証明の中身は実行時に不要だからです。
そのため、コンパイル後のコードには残りません。
4.2. 型を命題、その型に属する項を証明として読む
ここで見方を一つ導入します。
「型を命題として、その型に属する項を証明として読む」というやり方です。
これをCurry–Howard対応と言います。
ややこしいですが、Propは、Boolのtrueやfalseのような実行時の真偽値とは別の話で、「証明が存在するかどうか」を扱う、型の世界の話です。
この型に属する項を構築できれば、その等式が成り立つことを証明したことになります。
この型に属する項が証明です。
4.3. rfl——型検査器が等式を計算で確かめる
「項を構築する」とは、「その型を持つ式を書く」ということです。
def x : Nat := 42: 型名 := 式 という形で、右辺がその型に属する項です。
Lean の世界では、型を持つあらゆる式を「項」と呼びます。42、true、fun n => n + 1、どれも項です。
「項（term）」は型理論の用語で、プログラミング文脈では「値」や「式」と呼ぶものにほぼ対応します。
逆に、1 + 1 = 3 という型には属する項を構築できません。
型の定義上、どの値も取れないからです
証明できない命題は、型に項を入れられないという形で弾かれます。
つまり、「0は加法の単位元で足しても変わらない」と証明するには、 n + 0 = n という型に属する項を構築できればよいわけです。
def add_zero : (n : Nat) → n + 0 = n := fun n => rfl
-- ^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^
-- 変数 この部分が型 項
-- あるいは、
theorem add_zero (n : Nat) : n + 0 = n := rfl
-- ^^^^^^^^ ^^^^^^^^^ ^^^
-- 引数の型 この部分が型 項Code language: PHP (php)このコードでは、型 (n : Nat) → n + 0 = n の変数 add_zero を、fun n => rfl という関数オブジェクトで定義しています。
このコードが、コンパイラを無事に通るかどうか、それがポイントです。
このときに、使うのが rfl です。rfl は型「n = n 」に属する項で、「型検査器が両辺を計算すると同じ値になる」 Prop型の項になれます。
型検査器の動作をステップでみると、まずコードを受け取ると、両辺を正規形まで簡約して一致を確かめます。n + 0 の部分を、Nat.addの定義を元に簡約します。
rfl の検査ステップ:
目標の型 n + 0 = n
↓ 左辺を簡約
Nat.add の定義より n + 0 は n に簡約される
↓ 両辺を比較
n = n ── 一致
↓
rfl の型付け成功 ── 証明完了Nat.add は再帰で定義されていて、n + 0 の場合は定義そのものが n を返します。
型検査器はその計算を実行して n = n を確認します。rflは、この型の項として型検査に通ります。
一方、1 + 1 = 3 に rfl を使うと型検査は失敗します。
theorem wrong : 1 + 1 = 3 := by
rfl -- エラー：2 ≠ 3左辺を簡約すると 2、右辺は 3で、一致しないので、rflはこの型の項ではありません。
つまり、これは Int型の変数として 2.4 を入れたようなもので、型検査に失敗します。
証明できない命題は、この型に属する項を構築できないという形で弾かれます。
ただ、「証明できない命題」と「命題が偽である」ということは違います。
Leandは、項が構築できたとき、その型が空でないことはわかります。
しかし逆に、項が構築できなかったからといって、型が空であるとは言えないからです。
5. 型と命題の対応
等式型と rfl の感触が得られたところで、これを整理して型と命題の対応を表にします。
型と証明の対応（Curry–Howard 同型）:
プログラムの世界 証明の世界
─────────────────────────────
型 A 命題 A
値 a : A 証明 a : A
関数型 A → B 含意「A ならば B」
ペア型 A × B 連言「A かつ B」
依存関数型 (x:A) → B x 全称「すべての x:A について B x」
依存ペア型 Σ x:A, B x 存在「ある x:A について B x」Code language: CSS (css)ここで、「型に属する項」を示せれば、「命題が正しい」と言えます。
型に属する項を構築することが証明を与えることで、型検査が通ることが証明の正しさの確認です。
5.1. 含意——証明を引数として受け取る
次は、関数型 A → B が、証明での含意に対応する、ということの意味を順番に見ていきます。
まず、含意「A ならば B」の証明とは何かを考えます。
「A が成り立つと仮定したとき、B が成り立つ」を示すことです。
これは「A の証明を受け取って B の証明を返す」操作と同じです。
これを関数と捉え直します。
-- 「n = m ならば n + 1 = m + 1」を証明する
theorem succ_eq (n m : Nat) (h : n = m) : n + 1 = m + 1 := by
rw [h]引数 h : n = m に注目してください。n = m は型で、h はその型に属する項、つまり「n = m の証明」です。
通常の関数が n : Nat（自然数）を引数に取るように、この関数は h : n = m（等式の証明）を引数に取っています。
5.2. タクティクとエラボレーター
この複雑な型を満たす項は複雑になり、人間が手で書くのは困難です。
そこで使うのが、「タクティク」です。
よく使うタクティクをいくつか挙げると、
rflは両辺を計算して一致を確認、rw [h]は仮定hを使って書き換え、induction nはnに関する帰納法の適用、simpは既知の補題を使った自動簡約です。
by のブロックに入るとタクティクモードになります。
「タクティク（tactic）」というのは、証明を構築するための命令です。
エラボレーターはタクティクを解釈して、核言語の項に変換します。
VS Codeのlean4拡張では、カーソルを各行に置くと残りのゴールが表示されるので、対話的に項を構築していくことができます。
rw [h] は、 h を使ってゴールの n を m に書き換えるタクティクで、書き換え後のゴールは m + 1 = m + 1 になり、rfl で閉じられます。
含意の証明 = 関数の定義:
引数 h : (n = m) ← 仮定の証明を受け取る
戻り値 n + 1 = m + 1 ← 結論の証明を返す
「A ならば B」の証明
= 「A の証明を受け取って B の証明を返す関数」エラボレーターは、「型を知っているプリプロセッサ」みたいな感じだね。
5.3. エラボレーターとカーネル
Leanのコンパイラでは、型推論と型検査は分かれています。
それが、エラボレーターとカーネルです。
Lean の内部処理は、大きく4層に分かれています。
┌──────────────────────
│ 表面構文（Surface Syntax） │ 人間が書く
│ do 記法、タクティク、糖衣構文など │
└───────────────────┬──
↓ 変換
┌─────────────────────────
│ エラボレーション（Elaboration） │ 賢いが複雑
│ 型推論、暗黙引数挿入、制約解決、 │
│ タクティクを核言語の項に展開 │
└───────────────────┬─────
↓ 核言語の項
┌────────────────────────
│ カーネル（Kernel） │ 小さく正直
│ 型付けの最終確認だけを行う │
│ ここが壊れていなければ証明は正しい │
└───────────────────┬────
↓
┌────────────────────────
│ 実行系 │
│ コンパイル・最適化・実行 │
└────────────────────────Code language: JavaScript (javascript)エラボレーションではユーザーが触れる機能のほとんどを担っていて、穴 ?_ を埋めるための制約解決や、タクティクブロックを項に変換する処理がここに入ります。
-- タクティクで書いた証明（表面構文）
theorem add_zero (n : Nat) : n + 0 = n := by
induction n with
| zero => rfl
| succ n ih => simp [Nat.succ_add, ih]Code language: JavaScript (javascript)エラボレーターは、「型推論・暗黙引数の挿入・タクティクの展開」の複雑な操作をしますが、その分不具合が混入するおそれがあります。
そこで、型検査は、シンプルなカーネルで最終確認をします。
タクティクを使って証明を書いても、最終的にカーネルに渡るのはエラボレーターの生成した核言語の項です。
カーネルはその項の型付けを、計算を含む型検査で確かめます。
theorem add_zero (n : Nat) : n + 0 = n :=
Nat.rec
rfl
(fun n ih => by simp [Nat.succ_add, ih])
nCode language: PHP (php)「エラボレーションが賢く、カーネルが正直」という分業が Lean の信頼性の仕組みです10。
6. 例題：「フィボナッチ数列の隣接する2項は互いに素」
それでは、「フィボナッチ数列の隣接する2項は互いに素」という命題の証明を、Leanで検証してみます。
これは帰納法と補題の組み合わせが出てくるので、証明の構造が見えやすいです。
まずは、証明の筋道を確認します。
「fib n と fib (n+1) は互いに素」を数学的に証明するとき、帰納法を使います。gcd(fib n, fib(n+1)) = 1 を示したいのですが、鍵になるのは gcd(fib n, fib(n+1)) = gcd(fib(n+1), fib(n+2)) が成り立つことです。
フィボナッチの定義 fib(n+2) = fib(n+1) + fib(n) と gcd(a, b) = gcd(b, a mod b) を組み合わせると、gcdが帰納的に不変であることが言えます。
これをLeanで書くとこうなります。
import Mathlib.Data.Nat.GCD.Basic
import Mathlib.Data.Nat.Fib.Basic
-- フィボナッチ数列の隣接する2項の最大公約数は1（互いに素）
lemma fib_gcd (n : ℕ) : Nat.gcd (Nat.fib n) (Nat.fib (n + 1)) = 1 := by
induction n with
| zero =>
simp [Nat.fib]
| succ n ih =>
rw [Nat.fib_add_two]
rw [Nat.gcd_comm]
rw [Nat.gcd_add_self_right]
exact ihCode language: JavaScript (javascript)このコードでは、Nat.gcd_commやNat.fib_add_twoという補題を使うために、Mathlibという数学ライブラリからモジュールをインポートしています。
Mathlibには、数学の定理や補題が大量に収録されていて、gcdに関する定義と補題、フィボナッチ数列に関する定義と補題を使っているのです。
rwでは、これら既存の補題を使って、変換しています。
各ステップで何をしているかを追うと、まず inductionは、base caseとinductive stepに分けて考えます。
base case:
gcd(fib 0, fib 1) = gcd(0, 1) = 1 ← simp が計算する
inductive step:
gcd(fib(n+1), fib(n+2))
= gcd(fib(n+1), fib(n+1) + fib(n)) ← fib の定義を展開
= gcd(fib(n+1), fib(n)) ← gcd(a, a+b) = gcd(a, b)
= gcd(fib(n), fib(n+1)) ← 対称性
= 1 ← 帰納法の仮定 ihCode language: JavaScript (javascript)6.1. まとめ
出発点はコンパイラの型検査で、終着点が数学の形式証明です。
型検査の中で計算が走る
↓
値に依存した型が書ける（依存型）
↓
等式を型として書ける（等式型）
↓
型に属する項を構築する = 命題を証明する
├───────────────────┐
↓ ↓
プログラム検証 命題証明
（assert を型に持ち上げる） （数学的命題を型で表す）
└─────────┬─────────┘
↓
同じ型検査の仕組みの上に乗っている途中に断絶はなく、型検査器が扱える対象を値まで広げていった結果として、命題証明が同じ枠組みの上に現れます。
- Lean は Leonardo de Moura らによって開発され、2021年に Lean 4 として再実装されました。Lean 4 は Lean 自身で書かれており、C コードを生成することで効率的な実行が可能です。2025年には ACM SIGPLAN Programming Languages Software Award を受賞しています。 – Lean (proof assistant) – Wikipedia
- Lean 4 のアーキテクチャは、パーサ・エラボレータ・タクティク・コード生成器をすべてユーザーが拡張可能な設計になっています。コンパイラのソースコード構成は
src/Lean/Parser/、src/Lean/Elab/、src/Lean/Compiler/などに分かれています。 – leanprover/lean4 | DeepWiki - Leanの型検査では、正規化と定義的等価の判定という限定された計算が実行でき、停止性・一貫性の制約があります
- C 標準（ISO C11）では、配列の範囲外アクセスは未定義動作（Undefined Behavior）として規定されています。未定義動作はプログラムの出力が規格上まったく保証されず、ガベージ値の読み取り、セグメンテーション違反、あるいは意図しないメモリ破壊など、コンパイラ・OS・ハードウェアによって挙動が異なります。 – Undefined behavior – cppreference.com
- これは厳密には不正確で、Cは「一般の値依存型」を持ちませんが、コンパイル時定数（compile-time constant）は扱われます。
- elan は rustup をベースにして Lean 向けに作られたバージョン管理ツールです。
leanおよびlakeバイナリを PATH に配置し、プロジェクトごとに適切な Lean バージョンを自動で切り替えます。 – GitHub – leanprover/elan #evalのほかに、型だけを確認する#checkコマンドも頻繁に使います。たとえば#check Nat.addと書くとNat.add : Nat → Nat → Natが表示されます。どちらも Lean のインタラクティブな開発スタイルの中心にあります。 – Theorem Proving in Lean 4- 依存型の理論的な基盤は、Per Martin-Löf が 1970 年代に構築した直観主義型理論（Martin-Löf Type Theory, MLTT）に遡ります。Lean はこの系譜を引く「帰納型を持つ構成の計算（Calculus of Constructions with inductive types）」を基礎としています。 – Theorem Proving in Lean 4 – Introduction
Fin nは Lean の標準ライブラリに含まれる型で、値iと証明h : i < nのペアとして定義されています。この型を使うことで、範囲チェックをコンパイル時に行う API を設計できます。Idris のFinや Agda の同名の型と同じ概念です。 – Lean 4 Standard Library – Fin- このアーキテクチャは「小さな信頼済みカーネル（small trusted kernel）」設計と呼ばれ、Coq や Agda など多くの証明支援系で採用されています。カーネルが最小限の処理しか行わないことで、検証に必要な信頼の範囲（Trusted Computing Base, TCB）を狭く保てます。 – The Lean 4 Theorem Prover and Programming Language