Lean (証明アシスタント)
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2025/05/03 14:20 UTC 版)
 Leanのロゴ | |
| パラダイム | 関数型プログラミング |
|---|---|
| 登場時期 | 2013年 |
| 開発者 |
Leonardo de Moura Lean FRO |
| 最新リリース | v4.19.0/ 2025年5月1日 |
| 型付け | 推論される, 強い, 静的 |
| 影響を受けた言語 |
ML Coq Haskell Prolog Rust Scheme |
| 影響を与えた言語 | koka |
| プラットフォーム | クロスプラットフォーム |
| ライセンス | Apache License 2.0 |
| ウェブサイト |
lean-lang |
Lean は、プログラミング言語の一つである。「衛生的でありながら非常に強力なメタプログラミングフレームワークを備えた純粋関数型プログラミング言語」であり、同時に「Calculus of Inductive Constructions (CIC) と呼ばれる依存型の一種に基づく定理証明支援系」でもあるという２つの顔を持つ。この、汎用プログラミング言語でありながら定理証明支援系でもあるという点は Lean の大きな特徴である。
Lean は純粋関数型プログラミング言語でありながら、標準でループや可変ローカル変数の構文を備えているほか、一定の条件の下で関数アクセスをフィールドアクセスのように書くことができるという構文上の特徴がある。また、「参照カウントに基づいて自動的に破壊的変更を行う」という、Functional but in-place と呼ばれる最適化を行う。総じて、従来の関数型言語のパフォーマンスと構文面における欠点を改善している。
また、定理証明支援系としての Lean は、Unicode の積極的な使用と高度な対話性、拡張性の高さによる構文定義の柔軟性により可読性と快適な UI を提供することにある程度成功しており、型システムの専門家や形式証明の研究者だけでなく、数学研究者や学生からも支持を集め、Mathlib という大規模な形式数学ライブラリを擁するに至った。
歴史
2013年: 開発開始
Lean はGitHubでホストされているオープンソースプロジェクトである。2013年にMicrosoft ResearchのLeonardo de Mouraによって立ち上げられた[1]。
Lean は最初の定理証明支援系ではない。Lean の開発時点で Coq や Agda など他の定理証明支援系は存在しており、Lean の言語仕様はそれらから大きく逸脱したものではない。新しい証明支援系を考案した理由として、次の２点がある[2]。
- 証明のホワイトボックス自動化ツールを開発するためのプラットフォームを作成すること- Z3 SMT ソルバの開発者でもある Leonardo de Moura は、標準的な SMT 実装の長所と同時に限界も痛感していた。特に SMT ソルバの設定を変更することができず、フリーサイズ(one-size-fits-all)な設計となっていることは、ブラックボックス的であり好ましくなかった。ホワイトボックスアプローチとは、ここではSMTソルバを構成する要素をユーザが必要に応じて組み替えたり再構成したりできるように公開することを指す。対話的定理証明支援系(interactive theorem prover, ITP)のタクティク言語は、ホワイトボックス化を実現するための自然な手段であり、オーダーメイドの自動化を迅速かつ段階的に開発することを可能にし、SMT と対話的定理証明の間のギャップを埋めることに役立つだろうと期待できた。
- 小さな型理論とカーネル - Lean という名前には、英語で「痩せている」とか「贅肉がない」という意味がある。Lean の基礎としては標準的な依存型理論(dependent type theory)を最小限の理論に圧縮したものが採用されているが、これが Lean という名前の由来である。タクティクは無限に発展・洗練させることが可能であるべきだが、タクティクの出力を検証するシステムの実装は可能な限り単純であるべきである。Lean の目指す「Lean らしさ」は、依存型理論の他の実装と比較して「より複雑な論理を、より単純なシステムで表現する」ことである。Lean が影響を受けかつ最も Lean に近い型理論を採用している Coq と比較すると、Lean は fixpoint 演算子や型システムに埋め込まれたモジュールシステムがないなどの違いがある。
2014年: Lean 0.1
最初のプロトタイプは Lean 0.1 (2014 年) である。Lean 0.1 では ML ライクな構文が導入され、それは後のすべての Lean のバージョンで継承されることになる。単純な simp タクティクが既にこのバージョンから存在した。帰納型のサポートはまだなく、手で公理(axiom)を追加する必要があった。Lean 0.1 では、Lua スクリプトによる構文と戦術の拡張がサポートされていたが、この部分は後の Lean 3 で削除されることになる[3]。
2015年: Lean 2
2015 年、Lean の最初の公式リリースである Lean 2 が発表された。帰納型の適切なサポートや組み込みタクティクの拡張など、欠けていた重要な機能が追加されたほか、主要な機能として Lean 2 ではホモトピー型理論 (HoTT) のサポートが追加された[3]。
2017年: Lean 3
最初にリリースされた比較的安定したバージョンは Lean 3 で、2017年の1月20日にリリースされた[4]。Lean 3 では、あまり使用されていなかった Lua による構文拡張機能が削除され、根本的に異なるアプローチが採用された。Lean 自体がプログラミング言語とされ、Lean 自体によりタクティクの定義やそのほかのメタプログラミングが可能になった。Lean 2 からのもう一つの大きな変更は、ホモトピー型理論 (HoTT) のサポートの廃止である。HoTT のサポートが廃止された理由としては、
- 証明無関係(proof irrelevance) の公理がないと、タクティクを効率的に実装するのが難しくなり、コードの重複が生じるという問題
- 当時 「book HoTT」と最近の計算的な Cubical Type Theory のどちらが望ましいか不明だったという問題
が挙げられる。また、Lean で数学を形式化するライブラリである mathlib がコミュニティ管理の 独立したプロジェクトとして分離された[3]。
バージョン3.4.2以降、Lean 3の開発は正式に終了し、Lean 4の開発が始まった。
2021年: Lean 4
2021年、Lean 4の最初のマイルストーンリリースが発表された[5]。C++ではなく Lean 自身によって再実装され、「Lean は定理証明支援系であると同時に、汎用プログラミング言語でもある」と標榜するようになった。
Lean 4 より以前のバージョンでは、次のような問題点が認識されていたが、Lean 4 では大幅に改善された[6]。
- Lean 3 での経験から、定理証明を上手く行うためにはメタプログラミングフレームワークを備え、高い拡張性を有することが重要であると認識されていた。しかし Lean 3 のシステムの多くの部分が、C++ で書かれた Lean 3 のソースコードを変更しない限り、ユーザには変更できなかった。
- Lean 3 メタプログラミングは仮想マシン解釈のオーバーヘッドにより非効率だった。これにより Lean 3 での自動証明は、C++ や OCaml のような効率的なコンパイラを持つ言語で実装された同様の自動証明とは競合できなかった。
Lean 4 は完全に拡張可能であり、パーサ、エラボレータ、タクティク、決定手続き(decision procedure)、プリティプリンタ、コードジェネレータを変更・拡張することができる。また Lean 4 は対話的証明のためにカスタマイズされた衛生的なマクロ(hygienic macro)を持つ。Lean の構文をユーザが改変する際に C++ コードに触れる必要はなくなった[6]。
さらに Lean 4 ではメモリ管理手続きが改善されたほか、テーブル解決に基づく新しい型クラス解決アルゴリズムが使用され、パフォーマンスが改善された。また、Lean 4 は functional but in-place と呼ばれる新しいプログラミングパラダイムに基づくようになった[6]。
Lean 4 には Lean 3 との後方互換性はない。Lean3 で開発されていた主要なライブラリとして、2017年ごろから開発が行われていた[7]mathlib が挙げられるが、コミュニティにより Lean4 への書き直しが行われた。これには100万行以上のコードを書き換える必要があったが、この移行作業は2023年7月に完了した[8]。
2023年: Lean FRO設立
2023年7月、Lean Focused Research Organization (FRO) が設立された。[9]形式数学革命のために、証明のUI改善、スケーラビリティの改善、証明の自動化といった問題に取り組むとしている。また2023年9月、最初のLean 4 の公式リリースが発表された[10]。
Leanの型システム
無矛盾性
非形式的な数学において一般的に基礎理論として採用されているのは ZFC 集合論と呼ばれる理論であるが、Lean で採用されている基礎理論は Calculus of Inductive Constructions [11] (省略して CIC と呼ばれる) であって、これとは異なる。
Lean の型システムの無矛盾性については、Lean 3 の時代の結果として、「
Lean はオブジェクト指向言語ではなく、オブジェクトやクラスに相当する概念は存在しないが、関数適用を「まるでフィールドにアクセスするかのように」書くことができる記法が用意されている。これは Nim 言語における Uniform Function Call Syntax に似ている。
同じく純粋関数型言語である Haskell とは異なり、Lean は正格評価である。つまり、関数を評価する前に関数に渡された引数をすべて評価する。 Leanでは帰納型を定義することができる。帰納型とは、「その型の項を得る関数（コンストラクタ）」を有限通り指定することで定まる型であり、Leanでは「その型の上の関数/述語を得る方法（再帰原理）」が同時に生成されることで帰納法が可能であることが保証される。
帰納型の最も簡単な例は、列挙型である。列挙型とはある定められた有限通りの値しか取らない型のことで、たとえばBoolはLeanの標準ライブラリで列挙型として定義されている。列挙型は、「コンストラクタが引数を取らない」という特別なケースの帰納型である。 コンストラクタは引数をとっても構わない。特にこれから定義しようとしている自分自身を引数に取ることも許されるので、再帰的なデータ型を定義することができる。再帰的な帰納型の最も簡単な例は、自然数である。自然数はLeanの標準ライブラリでは次のように定義されている。 この定義はペアノの公理に基づいており、すべての自然数はゼロもしくは他の自然数の後者であると述べている。ペアノの公理には「コンストラクタが単射」「コンストラクタの像が重ならないこと」「帰納法の原理」も含まれるが、それらの成立はLeanによって自動的に保証される。
自然数の加算はパターン・マッチングを使用して、再帰的に定義できる。 Lean ではカリーハワード同型対応を利用して証明を行う。ある命題
これは Lean で簡単な命題の証明項を実際に構成した例である。 Lean の機能として、タクティクによって証明項を構成することができる。
Lean は依存型を持つ。つまり、関数 依存型がなければ命題（これは一種の型である）が項に依存することができないので、表現することができる命題の範囲がとても狭まってしまう。定理証明支援系をプログラミング言語として実現するうえで、依存型があることはとても重要な役割を果たす。
また、依存型はより柔軟にプログラムに型を付けることを可能にし、型で表現できるソフトウェアの仕様の範囲を広げる。以下は「長さが
Lean は強力なメタプログラミング機能を持っており、新しい記法の定義や証明の自動化が行えるようになっている。以下は、
Lean は対話的に証明を書くことをサポートするだけでなく、タクティクによる自動証明機能も提供する。以下は複雑な命題に見えるが、たった一つのタクティクで証明が終了する例である。 また次は、直観主義論理（排中律を仮定しない論理）における証明を自動で行ってくれるタクティクの例である。 Agda や Coq, Isabelle などの他の定理証明支援系と比べると Lean にはどのような特徴があるだろうか。この中で Isabelle は依存型がなく、依拠している基礎が異なるという著しい差異がある。Agda と Coq と比較すると、基礎はほぼ同じであるが、Lean には以下のような特徴がある。
型クラスは、プログラミングと定理証明の両方において、アドホック多相性 [17] を実現してくれる。しかし、Lean の急成長中の数学ライブラリ Mathlib の中で、型クラスが広く使われるにつれ既存の型クラス解決手続きの理論的限界が進歩の妨げになるようになった。既存の型クラス解決手続きの主要な理論的限界とは、次のようなものである：
Lean 4 では、この２つの問題を解決する新しいアルゴリズムであるテーブル化型クラス解決が実装されている。このアルゴリズムは Prolog に対して1998年に [18] 提案された型クラス解決アルゴリズムに基づく[16]。
Lean は純粋関数型言語であるため、手続き型言語では暗黙に扱われる副作用を、モナドという再利用可能な抽象的要素で再定義することで扱っている。この再定義によって、副作用をより厳密に制御したり、派生的な副作用を導入したりすることを可能にしている。モナドは Haskell の最もよく知られた抽象化機能であり、そのユビキタスな糖衣構文である do 記法と常に結びついている。
Lean では、メタプログラミングフレームワークによる高い拡張可能性を生かして、do 構文が Haskell と比べて拡張されている。具体的には以下のような記法を最初からサポートしている[19]。
たとえば、以下は Lean 4 で実装したエラトステネスの篩である。 ほとんどの関数型言語は、メモリ管理を自動で行うためにガベージ・コレクタを利用している。一方で、各値の正確な参照カウントを保持することで、破壊的更新などの最適化が可能になる。Lean は、純粋な関数型言語でありながら参照カウントを利用してメモリ管理を行う。参照カウントがちょうど１の値（つまり共有されていない値）を更新するとき、自動的に破壊的更新が行われる。このことを指して、Lean のプログラミングパラダイムのことを functional but in-place (FBIP) と呼ぶ[6]。特に、Lean で配列のようなデータ構造を扱うとき、FBIP によりコードの純粋性を保ちながら効率的なコードを生成することが可能である。
これにより Lean のコンパイラが生成するコードは効率的になり、 他の静的型付け言語と比較しても遜色のないものになった。
実際に Lean が値の破壊的変更を行っていることは、次のようなコードで確認することができる。 ITP（対話的定理証明支援系）において、構文を拡張可能にすることは複雑な数学的対象をわかりやすく表現するのに重要であるのみならず、ライブラリ開発においても再利用可能な抽象化を行うために役立つ。このように表現力の高いマクロシステムを持つことは ITP にとって極めて重要なのだが、Lean 3 のものを含め既存の ITP のマクロシステムには問題があった。
問題点は主に以下の２点である：
Lean 4 はこれらの問題を Scheme ファミリーに着想を得た新しいマクロシステムを開発することにより同時に解決した。新しいマクロシステムは、複数のマクロ抽象化レベルを単一で統一的なシステムで実装することを可能にし、高い表現力と安全性を両立した[21]。
たとえば、以下は Coq のライブラリ math-comp における和のΣ記号の定義である[22]。見てわかるように少しずつ異なる同様の定義が 12 回繰り返されている。 ほぼ同じことが Lean の数学ライブラリ mathlib4 では次のように表現されている[23]。明らかに繰り返しが少なく、簡潔な書き方になっていることがわかるだろう。 これは Lean では 
structure Point (α : Type) : Type where
x : α
y : α
-- アクセサ
#check (Point.x : {α : Type} → (Point α) → α)
#check (Point.y : {α : Type} → (Point α) → α)
def origin : Point Int := { x := 0, y := 0 }
-- 通常の関数適用の書き方
#guard Point.x origin = 0
-- フィールド記法。`.x` を付けるだけで値にアクセスできる
#guard origin.x = 0
正格評価
/-- 条件 `cond` が true なら最初の引数を，
false なら2番目の引数を返す関数 -/
def selectFst (cond : Bool) (fst snd : Nat) :=
if cond then
fst
else
snd
/-- 与えられた自然数をそのまま返す関数.
実行されると infoview に表示が出る. -/
def trace (n : Nat) : Nat :=
dbg_trace "trace is called"
n
/-
trace is called
10
-/
#eval selectFst true 10 (trace 20)
帰納型
inductive Bool where
| false
| true
inductive Nat : Type where
| zero : Nat
| succ : Nat → Nat
def Nat.add (n m : Nat) : Nat :=
match n with
| zero => m
| succ n => succ (add n m)
証明
P の証明 h は，型 P を持つような項 h : P と同一視される。したがって、Lean を仲介することによって「証明する」ということは、「正確にある型を持つような項を作る」ということに言い換えられる。
theorem and_swap (P Q : Prop) : P ∧ Q → Q ∧ P :=
fun h => { left := h.right, right := h.left }
by キーワードによってタクティクモードに入ることができる。タクティクモードの中では、「現在利用できる仮定や命題」「今示すべきこと」が常に infoview に表示され、対話的に証明を書くことができる。theorem and_swap (P Q : Prop) : P ∧ Q → Q ∧ P := by
-- P ∧ Q と仮定する
intro h
-- Q ∧ P を示すには Q と P をそれぞれ示せばよい
constructor
-- Q を示す
case left =>
exact h.right
-- P を示す
case right =>
exact h.left
依存型
f : A → B があったときに、f による t : A の返り値 f t の型が t に依存していてもよい。このとき f の型を f : (t : A) → B のように表記する。これにより、命題に正しく型を付けることが可能である。theorem one_add : ∀ n, n + 1 ≥ 1 := by simp_arith
/-
one_add 1 : 1 + 1 ≥ 1
-/
#check one_add 1
/-
one_add 3 : 3 + 1 ≥ 1
-/
#check one_add 3
n であるようなリスト」を Subtype として表現する型である。def Vect (α : Type) (n : Nat) : Type := {l : List α // l.length = n }
拡張可能性
notation コマンドで記法を定義する例である。def modulo (k n m : Int) : Prop := k ∣ (n - m)
-- modulo を二項関係らしく書けるようにする
notation:55 x:55 " ≃ " y:55 " mod " k:55 => modulo k x y
#check (1 ≃ 6 mod 5)
declare_syntax_cat コマンドや macro_rules コマンドを使うことで、さらに複雑な構文も定義することができる。[15]/-- 2項演算の集合 -/
inductive Op where
/-- 加法 -/
| add
/-- 乗法 -/
| mul
deriving BEq
/-- 数式 -/
inductive Expr where
/-- 数値リテラル -/
| val (n : Nat)
/-- 演算子の適用 -/
| app (op : Op) (left right : Expr)
deriving BEq
namespace Expr
/- ## Expr の項を定義するための見やすい構文を用意する -/
/-- `Expr` のための構文カテゴリ -/
declare_syntax_cat expr
/-- `Expr` を見やすく定義するための構文 -/
syntax "expr!{" expr "}" : term
syntax:max num : expr
syntax:30 expr:30 " + " expr:31 : expr
syntax:35 expr:35 " * " expr:36 : expr
syntax:max "(" expr ")" : expr
macro_rules
| `(expr!{$n:num}) => `(Expr.val $n)
| `(expr!{$l:expr + $r:expr}) => `(Expr.app Op.add expr!{$l} expr!{$r})
| `(expr!{$l:expr * $r:expr}) => `(Expr.app Op.mul expr!{$l} expr!{$r})
| `(expr!{($e:expr)}) => `(expr!{$e})
-- 構文が正しく動作しているかテスト
#guard
let expected := Expr.app Op.add (app Op.mul (val 1) (val 2)) (val 3)
let actual := expr!{1 * 2 + 3}
expected == actual
end Expr
自動証明
example (a₁ a₂ a₃ : Nat) : 3 ∣ a₁ + 10 * a₂ + 100 * a₃ ↔ 3 ∣ a₁ + a₂ + a₃ := by
omega
import Mathlib.Tactic.ITauto
/-- 排中律の二重否定 -/
example (P : Prop) : ¬¬ (P ∨ ¬ P) := by
intro h
apply h
have : ¬ P := by
intro hp
have : P ∨ ¬ P := by left; assumption
contradiction
right
assumption
example (P : Prop) : ¬¬ (P ∨ ¬ P) := by
itauto
Lean の特徴
テーブル化型クラス解決(Tabled Typeclass Resolution)
拡張された do 記法
let mut で宣言できるようにする Rust ライクな記法for ループ、break や continue といった制御フロー/-- `n`以下の素数のリストを `Array Bool` の形で返す。
`i` 番目が `true` ならば `i` は素数で、`false` ならば合成数。 -/
def eratosthenesAux (n : Nat) : Array Bool := Id.run do
let mut isPrime := Array.replicate (n + 1) true
isPrime := isPrime.set! 0 false
isPrime := isPrime.set! 1 false
for p in [2 : n + 1] do
if not isPrime[p]! then
continue
if p ^ 2 > n then
break
-- `p` の倍数を消していく
let mut q := p * p
while q ≤ n do
isPrime := isPrime.set! q false
q := q + p
return isPrime
/-- エラトステネスの篩 -/
def eratosthenes (n : Nat) : Array Nat :=
eratosthenesAux n
|>.zipIdx
|>.filterMap fun ⟨isPrime, i⟩ =>
if isPrime then some i else none
#guard eratosthenes 10 = #[2, 3, 5, 7]
#guard
let actual := eratosthenes 100
let expected := #[
2, 3, 5, 7, 11,
13, 17, 19, 23, 29,
31, 37, 41, 43, 47,
53, 59, 61, 67, 71,
73, 79, 83, 89, 97
]
expected == actual
Functional but in-place
-- Lean のオブジェクトのメモリ上でのアドレスを取得する関数
-- 参照透過性を壊すため，unsafe である
#eval ptrAddrUnsafe #[1, 2, 3]
/-- フィボナッチ数列を計算する -/
def fibonacci (n : Nat) : Array Nat := Id.run do
-- 可変な配列 `fib` を宣言している
let mut fib : Array Nat := Array.mkEmpty n
fib := fib.push 0
fib := fib.push 1
for i in [2:n] do
-- ここで配列 `fib` のメモリアドレスを表示させている
dbg_trace unsafe ptrAddrUnsafe fib
fib := fib.push (fib[i-1]! + fib[i-2]!)
return fib
-- 値がコピーされていれば異なるメモリアドレスが表示されるはずだが...?
#eval fibonacci 15
衛生的でありながら強力なメタプログラミングフレームワーク
Reserved Notation "\sum_ i F"
(at level 41, F at level 41, i at level 0,
right associativity,
format "'[' \sum_ i '/ ' F ']'").
Reserved Notation "\sum_ ( i <- r | P ) F"
(at level 41, F at level 41, i, r at level 50,
format "'[' \sum_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\sum_ ( i <- r ) F"
(at level 41, F at level 41, i, r at level 50,
format "'[' \sum_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\sum_ ( m <= i < n | P ) F"
(at level 41, F at level 41, i, m, n at level 50,
format "'[' \sum_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\sum_ ( m <= i < n ) F"
(at level 41, F at level 41, i, m, n at level 50,
format "'[' \sum_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\sum_ ( i | P ) F"
(at level 41, F at level 41, i at level 50,
format "'[' \sum_ ( i | P ) '/ ' F ']'").
Reserved Notation "\sum_ ( i : t | P ) F"
(at level 41, F at level 41, i at level 50). (* only parsing *)
Reserved Notation "\sum_ ( i : t ) F"
(at level 41, F at level 41, i at level 50). (* only parsing *)
Reserved Notation "\sum_ ( i < n | P ) F"
(at level 41, F at level 41, i, n at level 50,
format "'[' \sum_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\sum_ ( i < n ) F"
(at level 41, F at level 41, i, n at level 50,
format "'[' \sum_ ( i < n ) '/ ' F ']'").
Reserved Notation "\sum_ ( i 'in' A | P ) F"
(at level 41, F at level 41, i, A at level 50,
format "'[' \sum_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\sum_ ( i 'in' A ) F"
(at level 41, F at level 41, i, A at level 50,
format "'[' \sum_ ( i 'in' A ) '/ ' F ']'").
syntax bigOpBinder := term:max ((" : " term) <|> binderPred)?
syntax bigOpBinderParenthesized := " (" bigOpBinder ")"
syntax bigOpBinderCollection := bigOpBinderParenthesized+
syntax bigOpBinders := bigOpBinderCollection <|> (ppSpace bigOpBinder)
syntax (name := bigsum) "∑ " bigOpBinders ("with " term)? ", " term:67 : term
syntax および declare_syntax_cat というコマンドが用意されていることと関係がある。Lean ではユーザが構文カテゴリを定義し、パーサの拡張を抽象化された高水準言語で行うことができる。これは Lean 3 までの静的なマクロでは不可能だった。
利用
脚注
関連項目
外部リンク
× に対する \times のようなLaTeXに似たシーケンスを使用して入力ができるようにする。
- Lean (証明アシスタント)のページへのリンク
