はじめての Lean 4 証明五手で1つの定理を証明する — インストール不要・10分・スマホでも動く

LeanDFumt チュートリアル · ブラウザ内で静的に動作

証明支援系 (proof assistant) は「解く」ソフトウェアではなく、「認める」ソフトウェアです。あなたが書いた手数を1つずつ検査し、正当なものだけを受理し、それ以外は拒絶します。このページでは、その仕組みを外から実感するために、小さな定理を1つ、五手で証明していきます。

ここで起きること

Lean 4 は、Microsoft Research で生まれ、現在は Lean FRO が保守している証明支援系です。証明を実際に検査する信頼カーネル (trusted kernel) は約3万行の C++ で書かれています。Lean で書かれた数学のほぼ全て — そして、これから世界中で書かれる証明 — は、最終的にこのカーネルが受理する項へと還元されます。

これから証明する定理は1つ、任意の自然数 n について、左に 0 を足すと n に戻る という命題です。信じるのは簡単です。しかし、加法の定義から出発し、手抜きなしで、機械が検査できる形で証明するには、五手が必要です。

各ステップのコードの下にあるのは、Lean の InfoView — 証明支援系が「まだ残っている目標 (goals)」を教えてくれる欄 — を模したパネルです。このパネルを注視してください。ここに Goals accomplished と表示されたとき、定理は証明されたことになります。

証明する定理

theorem zero_add

∀ n : Nat, 0 + n = n

任意の自然数 n について、0 + n は n に等しい

証明 — 一手ずつ

ステップ 1 / 5 残り目標: 1

STEP 1 — 目標を宣言する
```
theorem zero_add (n : Nat) : 0 + n = n := by
  -- ここに証明を書く
  sorry
```
目標 (1件)

n : Nat ⊢0 + n = n

定理に名前をつけ、内容を宣言し、by ブロック — 戦術 (tactic) による証明 — を開きます。sorry は「まだ書いていない証明の代わり」を意味するプレースホルダです。InfoView には目標が1つ表示されています: 自然数 n が与えられたとき、0 + n = n を示せ、と。
STEP 2 — n について帰納法を適用する
```
theorem zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero => sorry
  | succ k ih => sorry
```
目標 (2件)

基底ケース (case zero)
⊢0 + 0 = 0

帰納ステップ (case succ)
k : Nat ih : 0 + k = k ⊢0 + Nat.succ k = Nat.succ k

帰納法は証明を2つに分けます。基底ケースは n = 0 のときの主張を示すことを要求し、帰納ステップは「ある k について定理が成立している」という仮定 — これが ih、帰納法の仮定 です — の下で、k + 1 についても示せ、と要求します。
STEP 3 — 基底ケースを閉じる
```
theorem zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih => sorry
```
目標 (1件)

帰納ステップ (case succ)
k : Nat ih : 0 + k = k ⊢0 + Nat.succ k = Nat.succ k

rfl は reflexivity (反射律) の略で、両辺が 定義上等しい 任意の目標を閉じます。Lean は加法を定義する際に、0 + 0 が 0 にそのまま簡約されるように作られています。追加の作業なしで基底ケースは閉じます。目標が1つ減り、残り1つになりました。
STEP 4 — 後者を展開する
```
theorem zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih => rw [Nat.add_succ]
```
目標 (1件)

帰納ステップ (case succ)
k : Nat ih : 0 + k = k ⊢Nat.succ (0 + k) = Nat.succ k

補題 Nat.add_succ は a + Nat.succ b を Nat.succ (a + b) に書き換える等式です。戦術 rw はこの書き換えを目標に左から右へ適用します。目標の形が変わったことに注目してください: 今や証明すべきは Nat.succ (0 + k) = Nat.succ k です。
STEP 5 — 帰納法の仮定を適用する
```
theorem zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih => rw [Nat.add_succ, ih]
```
Goals accomplished — すべての目標が達成されました

残り目標なし · 定理は証明されました

仮定 ih — 「0 + k = k」 — で書き換えると、目標は Nat.succ k = Nat.succ k に縮み、Lean はこれを反射的に閉じ、証明全体を完了します。InfoView は空になりました。定理を通るすべての経路が検査されたということです。

いま何が起きたのか

あなたが書いた各ステップは、Nat、0、+、= の定義に照らしてリアルタイムに検査されました。テストは1本も走っていません。ファジングもしていません。検査器は証明全体を型理論の公理まで還元し、結果として得られた項が型検査を通ることを確認しました。この定理がいま真であるのは、誰かが信じているからではなく、真であることを否定するためには Lean のカーネルそのものを反証する必要があり、それは私たちが解いた問題よりずっと難しいから、です。

これが形式検証の原子操作です。この規模は上に伸びます。暗号プロトコル、コンパイラのパス、分散合意、そして — 増えつつあるのが — AI エージェントの挙動が、こうして1定理ずつ証明されています。あなたがいま見たものは、玩具の問題にしか通用しない玩具ではありません。同じ機械の入口です。

次に読むもの

Theorem Proving in Lean 4 (日本語訳) — aconite-ac さんによる包括的な日本語訳。本を1冊読み切る覚悟がある方に
Natural Number Game (英語) — ブラウザ内で最初の100定理を証明できるゲーム。インストール不要
Theorem Proving in Lean 4 (英語原著) — Avigad、de Moura、Kong、Ullrich による正典的入門
LeanDFumt · D-FUMT₈ — Mathlib 非依存・pure Lean 4 で書かれた8値論理の zero-sorry ライブラリ (29定理)。関連読み物として Agent verification, formally (英語ノート) とエラー辞書 (英語) があります。
Your first Lean 4 proof (English original) — このページの英語版

はじめての Lean 4 証明 五手で1つの定理を証明する — インストール不要・10分・スマホでも動く