背景

• 最近はLeanという言語をニュースでよく見る
• IUT理論での証明や、テレンス・タオが使っていたりする
• Leanが、どのようにTruth and proofをやってくれるのかが気になった
• そこで、Leanがどんなものか試してみた

Lean

Leanとは

Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code

一言で言えば、ブラジルの科学者によって作成された証明を形式化したプログラミング言語。

Leanが何に使われているのか

Lean is the core verification technology behind Cedar, the open-source authorization language that powers cloud services like Amazon Verified Permissions and AWS Verified Access. Our team rigorously formalizes and verifies core components of Cedar using Lean’s proof assistant, and we leverage Lean’s lightning-fast runtime to continuously test our production Rust code against the Lean formalization. Lean’s efficiency, extensive libraries, and vibrant community enable us to develop and maintain Cedar at scale, while ensuring the key correctness and security properties that our users depend on.

• AWSでも使われているらしい
• 例えば、Amazon Verified Permissionsは内部でCedarというPolicy言語を使っている
• そのCedarを検証するために、Leanが使われているっぽい

Installation

• VS CodeでLean 4 Extensionを使ってそのままランタイムもインストールされた

Lean言語

Leanの感覚的な証明の流れ:

1
2
3
4
5
6
7

theorem 名前 : 証明したい命題 := by
  ゴールを分解する
  仮定を導入する
  既知の定理や仮定を使う
  書き換える
  単純化する
  全ゴールが消えたら証明完了

TypeとProp

Leanを理解するうえで重要な2種類の分類として、Type と Prop がある。

つまり、次のようにデータを扱う。

• 命題 = 型
• 証明 = その型の値

Leanでよく使われる命令

 1
 2
 3
 4
 5
 6
 7
 8
 9
10

intro       -- 仮定を導入
exact       -- ぴったりの証明を渡す
apply       -- 定理や関数を適用
constructor -- ∧ や ↔ などを分解
cases       -- 場合分け
induction   -- 帰納法
rw          -- 等式で書き換え
simp        -- 自動で単純化
ring        -- 多項式計算を自動証明
linarith    -- 線形不等式を自動証明

tacticとは

• タクティクは、Lean において証明を対話的に行ったり自動化したりすることを可能にするもの
• ようは、tactic は、Leanの証明ゴールを少しずつ攻略するコマンドみたいなんもの

Curry-Howard対応とは

命題とプログラムの型は同じ構造をしているという関係対応。

Curry-Howardの例

例：「AならばB」の証明

論理的には：

1

A が真 → B が真

Leanでは：

1
2

fun (a : A) => ... : B
-- A型の値を受け取って B型の値を返す関数

関数を定義すること＝「AならばBを証明すること」 になる。

別の言い方だと、「引数を渡す」というプログラム操作が、そのまま「命題を適用する」論理操作になっている。

Leanの証明の型一覧

ゴールの形によって、必要な証明の構造が変わる。

覚え方:

1
2
3
4
5

∧ (かつ)  → 両方必要  → ペア ⟨_, _⟩
∨ (または) → どちらか  → Or.inl か Or.inr
∀ (すべて) → 関数      → fun x => ...
∃ (ある)  → 具体例    → ペア ⟨witness, _⟩
¬ (でない) → 矛盾へ    → fun a => False

Leanの例

三段論法

三段論法：

• すべての人間は死ぬ
• ソクラテスは人間である
• よって、ソクラテスは死ぬ

1
2
3
4
5
6
7
8
9

theorem syllogism
  {Person : Type}
  (Human : Person → Prop)
  (Mortal : Person → Prop)
  (socrates : Person)
  (hAll : ∀ x : Person, Human x → Mortal x)
  (hSocrates : Human socrates) :
  Mortal socrates := by
  exact hAll socrates hSocrates

キーワードの意味:

• Person: 人の集合みたいなもの
• Human: その人が人間かどうか
• Mortal: その人が死すべき存在かどうか
• socrates: ソクラテス
• hAll: 任意の x について、Human x なら Mortal x
• hSocrates: Socrates は Human
• 結論: Socrates は Mortal

つまり、下のような関係になっている。

1
2
3

「Human socrates → Mortal socrates」という命題
        ↕ 同じ構造
「Human socrates を受け取って Mortal socrates を返す関数」

最後にexactは「この値がゴールの型とぴったり一致します」とLeanに渡すだけで、実行というより値を提出するイメージ。

ペアノの公理

1
2
3
4
5

-- 任意の自然数 n に対して、n より大きい自然数が存在する
theorem nat_has_no_maximum :
  ∀ n : Nat, ∃ m : Nat, n < m := by
  intro n
  exact ⟨Nat.succ n, Nat.lt_succ_self n⟩

意味は以下の証明になる。

• 任意の n について、
• m = succ n を取れば、
• n < m である

exact ⟨Nat.succ n, Nat.lt_succ_self n⟩の意味:

つまり、次を意味する。

1
2

Nat.lt_succ_self : ∀ n : Nat, n < Nat.succ n
-- すべての自然数 n について、n < n+1 が成り立つ

まとめ

• そもそもゲーデルの不完全性定理では、無矛盾かつ完全な形式体系はなく、証明できないものがあると証明されていたはず
• つまり、どの系の形式化や一般化でも証明できないものがあるはず
• ただ、証明はできないものがあるが、Leanを通せば証明を検証・形式化できるのはAI時代には有用かもしれない

参考文献

• Lean Programming Language
• タクティク - Lean by Example