はじめに
最近、数学界の超難問であるABC予想の証明の正しさを検証するために、定理証明支援系 Lean を利用するというニュースが話題を呼んだ。1
私自身 Lean という名前を耳にする機会は増えたものの、実際に触れたことはなかった。
本記事では Lean を用い、自然数と加算を定義した上で、 $1 + 1 = 2$ の証明、および加法の結合法則 $(a + b) + c = a + (b + c)$ の証明を行う。
定理証明支援系、 Lean とは？
定理証明支援系とは、数学の定義・定理・証明をプログラムのように記述し、その論理的な正しさをコンピュータが厳密にチェックするソフトウェアである。
人間による証明では明らかであると省略されがちなステップも、コンピュータ上ではすべて明示しなければならず、一切の曖昧さが許されない。
Lean は、Microsoft Research で開発が始まった、オープンソースの定理証明支援系である。
依存型理論をベースとして数学的証明を厳密に検証できるだけでなく、関数型プログラミング言語としても利用できる点が特徴である。
Lean では、証明したい命題を「ゴール」として設定し、「タクティク」と呼ばれる操作を適用してそのゴールを段階的に書き換えていく。最終的に自明な命題（例えば、左辺と右辺が同じ形の等式）まで落とし込めれば、証明は完了となる。
定理証明支援系としては Lean の他に Coq や Isabelle 等がある。
Coq は四色問題の検証に使われたツールとして有名である。
Lean のインストール方法
公式ドキュメントに記載の通り、VS Code 経由で Lean の最新バージョン Lean 4 をインストールするのがおすすめである。
VS Code を用いると、ゴール表示・補完・エラー箇所のハイライト等の機能を利用でき、証明をより便利に進めることができる。
自然数と加法の定義
今回 $1+1=2$ を示したいが、そのためには自然数や加算を定義する必要がある。
ペアノの公理系に基づく自然数の定義
ここでは、ペアノの公理系に基づいて自然数を導入する、すなわち自然数は以下の5つの公理を満たすものとする。
- 自然数 $0$ が存在する2
- 後者関数 $\mathrm{succ}$ が存在する
- 直感的には、 $\mathrm{succ}(n)$ は $n$ の次の数を表す
- $\mathrm{succ}(0)$ を $1$ 、$\mathrm{succ}(1) = \mathrm{succ}(\mathrm{succ}(0))$ を $2$ と呼ぶ
- $\mathrm{succ}(n) \neq 0$
- $\mathrm{succ}$ は単射（ $\mathrm{succ}(m) = \mathrm{succ}(n)$ なら $m = n$ ）
- 数学的帰納法が成り立つ
- 命題 $P(n)$ に関し、 $P(0)$ と $P(n) \implies P(\mathrm{succ}(n))$ が成り立つならば、任意の自然数 $n$ で $P(n)$ が成り立つ
Lean では次のように表現できる。3
ここで、 MyNat は自然数の型を表し、 ∀ n : MyNat , P n は任意の自然数 n について P n が成り立つことを表す。
-- ペアノの公理系により自然数を定義
axiom MyNat : Type
axiom zero : MyNat
axiom succ : MyNat → MyNat
axiom succ_ne_zero : ∀ n : MyNat, succ n ≠ zero
axiom succ_injective : ∀ (m n : MyNat), succ m = succ n → m = n
axiom mynat_induction :
∀ (P : MyNat → Prop),
P zero →
(∀ n, P n → P (succ n)) →
∀ n, P n
自然数の加法の定義
次に、加法が満たすべき性質を以下の2つの公理によって規定し、自然数の体系に加法を導入する。4
- $n + 0 = n$
- $n + \mathrm{succ}(m) = \mathrm{succ}(n + m)$
2つ目は「$n + (m の次の数)$ は、$(n + m) の次の数$ である」という規則になっている。
Lean では次のように表現できる。
-- 加法を定義
axiom add : MyNat → MyNat → MyNat
axiom add_zero : ∀ n, add n zero = n
axiom add_succ : ∀ n m, add n (succ m) = succ (add n m)
1 + 1 = 2 の証明
準備が整ったところで、$1 + 1 = 2$ の証明を行う。
まず、$1$ と $2$ を以下のように定義する。5
-- 1, 2 を定義
noncomputable def one : MyNat := succ zero
noncomputable def two : MyNat := succ (succ zero)
証明したい命題は add one one = two である。
タクティク unfold（ある変数の定義そのものをその中身で置き換える）や rw（既知の等式 A = B を用いて、ゴール中にある A を B に置き換える）でゴールを段階的に変形していく。最終的に左辺と右辺が構文的に一致すれば、証明は完了する。
$1+1=2$ を証明する Lean のコードは以下のようになる。
証明したい命題を theorem として設定し、その後に適用するタクティクを記述していく。
各ステップにおけるゴールは （変数や仮定） ⊢ （証明すべき命題） という形で書かれている。
-- 1 + 1 = 2 を証明
theorem one_add_one_eq_two : add one one = two := by
-- (goal) ⊢ add one one = two
unfold one -- one を succ zero に置換
-- (goal) ⊢ add (succ zero) (succ zero) = two
unfold two -- two を succ (succ zero) に置換
-- (goal) ⊢ add (succ zero) (succ zero) = succ (succ zero)
rw [add_succ] -- 公理 n + succ(m) = succ(n + m) を適用
-- (goal) ⊢ succ (add (succ zero) zero) = succ (succ zero)
rw [add_zero] -- 公理 n + 0 = n を適用
-- (goal) ⊢ succ (succ zero) = succ (succ zero)
-- 左辺と右辺が同じ形になったので証明終了
VS Code の Lean 拡張を利用すれば、証明の各ステップで現在のゴールを常に確認できる。
そのゴールを見ながら、次に適用すべきタクティクを選択し、一つずつ適用していく。こうしてゴールの変形を繰り返し、最終的に自明な形（左辺と右辺が構文的に一致する等式）へと帰着させるのが、今回の証明の進め方である。
（途中経過）
（証明完了）
加法の結合法則の証明
次に、より複雑な例として、結合法則 $(a + b) + c = a + (b + c)$ を証明する。
証明の構成
変数 $c$ についての数学的帰納法を用いる。
- $c = 0$ の場合
add_zeroにより $(a+b)+0 = a+b$ と $b+0=b$ が従うから、
$(a+b)+0 = a+b = a+(b+0)$ が成り立つ。 - 帰納法の仮定として $(a+b)+n = a+(b+n)$ が成り立つと仮定する。
add_succにより
$(a+b)+\mathrm{succ}(n) = \mathrm{succ}((a+b)+n)$ と
$a+(b+\mathrm{succ}(n)) = a+\mathrm{succ}(b+n) = \mathrm{succ}(a+(b+n))$ が従う。
帰納法の仮定を適用して $(a+b)+\mathrm{succ}(n) = \mathrm{succ}((a+b)+n) = \mathrm{succ}(a+(b+n)) = a+(b+\mathrm{succ}(n))$
が成り立つ。
Lean での証明コード
-- 加法の結合法則を証明
theorem add_assoc (a b c : MyNat) : add (add a b) c = add a (add b c) := by
-- (goal) a b c : MyNat ⊢ add (add a b) c = add a (add b c)
apply mynat_induction (fun c => add (add a b) c = add a (add b c)) -- c に関する帰納法を適用
-- (goal) 次の2つを示せばよい
-- (1) a b : MyNat ⊢ add (add a b) zero = add a (add b zero)
-- (2) a b : MyNat ⊢ ∀ (n : MyNat), add (add a b) n = add a (add b n) → add (add a b) (succ n) = add a (add b (succ n))
· -- (1) base case
-- (goal) a b : MyNat ⊢ add (add a b) zero = add a (add b zero)
rw [add_zero] -- 公理 add_zero を用いて左辺を変形
-- (goal) a b : MyNat ⊢ add a b = add a (add b zero)
rw [add_zero] -- 公理 add_zero を用いて右辺を変形
-- (goal) a b : MyNat ⊢ add a b = add a b
-- 左辺と右辺が同じ形になったので証明終了
· -- (2) inductive step
-- (goal) a b : MyNat ⊢ ∀ (n : MyNat), add (add a b) n = add a (add b n) → add (add a b) (succ n) = add a (add b (succ n))
intro (n : MyNat) -- 「∀ (n : MyNat)」の ∀ を剥がして n を変数として取る
-- (goal) a b n : MyNat ⊢ add (add a b) n = add a (add b n) → add (add a b) (succ n) = add a (add b (succ n))
intro ih -- 「→」の前の仮定を ih として取る
-- (goal) a b n : MyNat
-- ih : add (add a b) n = add a (add b n)
-- ⊢ add (add a b) (succ n) = add a (add b (succ n))
rw [add_succ] -- 公理 add_succ を用いて左辺を変形
-- (goal) a b n : MyNat
-- ih : add (add a b) n = add a (add b n)
-- ⊢ succ (add (add a b) n) = add a (add b (succ n))
rw [add_succ] -- 公理 add_succ を用いて右辺を変形
-- (goal) a b n : MyNat
-- ih : add (add a b) n = add a (add b n)
-- ⊢ succ (add (add a b) n) = add a (succ (add b n))
rw [add_succ] -- 公理 add_succ を用いて右辺を変形
-- (goal) a b n : MyNat
-- ih : add (add a b) n = add a (add b n)
-- ⊢ succ (add (add a b) n) = succ (add a (add b n))
rw [ih] -- 帰納法の仮定 ih を用いて左辺を変形
-- (goal) a b n : MyNat
-- ih : add (add a b) n = add a (add b n)
-- ⊢ succ (add a (add b n)) = succ (add a (add b n))
-- 左辺と右辺が同じ形になったので証明終了
まとめ
Lean を用いることで、数学の証明をプログラムのデバッグに近い感覚で、厳密に進めることが可能になる。
数学を学習していて「本当にこの証明は正しいのか」と不安になることは多い。そうしたとき、 Lean のような定理証明支援系を利用して形式的に検証するのも有力な手段である。