Lean (証明アシスタント)

Lean
	Leanのロゴ
パラダイム	関数型プログラミング
登場時期	2013年 (11年前)
開発者	Leonardo de Moura; LeanFRO
最新リリース	v4.7.0/ 2024年4月3日 (53日前)
型付け	推論される, 強い, 静的
影響を受けた言語	ML; Coq; Haskell; Prolog; Rust
プラットフォーム	クロスプラットフォーム
ライセンス	Apache License 2.0
ウェブサイト	lean-lang.org
	テンプレートを表示

Lean は純粋関数型プログラミング言語のひとつである。また、同時に証明支援系(theorem prover)（英語版）でもある。帰納型（英語版）を伴うCalculus of constructions（英語版）と呼ばれる型システムに基づいている。純粋関数型言語であるが、functional but in-place と呼ばれるプログラミングパラダイムに基づいており、効率性を重視している。

歴史[編集]

2013年: 開発開始[編集]

Lean はGitHubでホストされているオープンソース（英語版）プロジェクトである。2013年にMicrosoft ResearchのLeonardo de Mouraによって立ち上げられた^[1]。

Lean は最初の定理証明支援系ではない。Lean の開発時点で Coq や Agda など他の定理証明支援系は存在しており、Lean の言語仕様はそれらから大きく逸脱したものではない。新しい証明支援系を考案した理由として、次の２点がある。^[2]

証明のホワイトボックス自動化ツールを開発するためのプラットフォームを作成すること- Z3 SMT ソルバの開発者でもある Leonardo de Moura は、標準的な SMT 実装の長所と同時に限界も痛感していた。特に SMT ソルバの設定を変更することができず、フリーサイズ(one-sizefits-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年: LeanFRO設立[編集]

2023年7月、Lean Focused Research Organization (FRO) が設立された。^[9]形式数学革命のために、証明のUI改善、スケーラビリティの改善、証明の自動化といった問題に取り組むとしている。また2023年9月、最初のLean 4 の公式リリースが発表された。^[10]

Lean の機能[編集]

対話的実行[編集]

プログラミング言語としての Lean は、関数などの式を部分的に実行して評価することが容易にできるように設計されている。#eval というコマンドが存在し，関数などをその場で評価することができる。

def frac (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | n + 1 => (n + 1) * frac n

-- エディタ上でコードを開いているとき
-- `#eval` の上にマウスオーバーすると 120 と表示される
#eval frac 5

正格評価[編集]

同じく純粋関数型言語である Haskell とは異なり、Lean は正格評価である。つまり、関数を評価する前に関数に渡された引数をすべて評価する。

/-- 条件 `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 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)

証明[編集]

Lean ではカリーハワード同型対応を利用して証明を行う。ある命題 P の証明 h は，型 P を持つような項 h : P と同一視される。したがって、Lean を仲介することによって「証明する」ということは、「正確にある型を持つような項を作る」ということに言い換えられる。

これは Lean で簡単な命題の証明項を実際に構成した例である。

theorem and_swap (P Q : Prop) : P ∧ Q → Q ∧ P := 
  fun h => { left := h.right, right := h.left }

Lean の機能として、タクティクによって証明項を構成することができる。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

依存型[編集]

Lean は依存型を持つ。つまり、関数 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

拡張可能性[編集]

Lean は強力なメタプログラミング機能を持っており、新しい記法の定義や証明の自動化が行えるようになっている。以下は、二項関係らしい記法をマクロとして定義した例である。ここで詳しくは述べないが、新しいタクティクやコマンドを定義することも可能である。

def modulo (k n m : Int) : Prop := k ∣ (n - m)

-- modulo を二項関係らしく書けるようにする
notation:55 x " ≃ " y " mod " k => modulo k x y

#check (1 ≃ 6 mod 5)

自動証明[編集]

Lean は対話的に証明を書くことをサポートするだけでなく、タクティクによる自動証明機能も提供する。以下は複雑な命題に見えるが、たった一つのタクティクで証明が終了する例である。

example (a₁ a₂ a₃ : Nat) : 3 ∣ a₁ + 10 * a₂ + 100 * a₃ ↔ 3 ∣ a₁ + a₂ + a₃ := by
  omega

Lean の特徴[編集]

テーブル化型クラス解決(Tabled Typeclass Resolution)[編集]

型クラスは、プログラミングと定理証明の両方において、アドホック多相性 ^[12] を実現してくれる。しかし、Lean の急成長中の数学ライブラリ Mathlib の中で、型クラスが広く使われるにつれ既存の型クラス解決手続きの理論的限界が進歩の妨げになるようになった。既存の型クラス解決手続きの主要な理論的限界とは、次のようなものである：

ダイアモンドが存在する場合、指数関数的に実行時間が伸びてしまう
サイクルが存在する場合に発散が生じる

Lean 4 では、この２つの問題を解決する新しいアルゴリズムであるテーブル化型クラス解決が実装されている。このアルゴリズムは Prolog に対して1998年に ^[13] 提案された型クラス解決アルゴリズムに基づく。 ^[11]

拡張された do 記法[編集]

Lean は純粋関数型言語であるため、手続き型言語では暗黙に扱われる副作用を、モナドという再利用可能な抽象的要素で再定義することで扱っている。この再定義によって、副作用をより厳密に制御したり、派生的な副作用を導入したりすることを可能にしている。モナドは Haskell の最もよく知られた抽象化機能であり、そのユビキタスな糖衣構文である do 記法と常に結びついている。

Lean では、メタプログラミングフレームワークによる高い拡張可能性を生かして、do 構文が Haskell と比べて拡張されている。具体的には以下のような記法を最初からサポートしている。^[14]

可変な変数を let mut で宣言できるようにする Rust ライクな記法
早期リターン(early return)
for ループ、break や continue といった制御フロー

利用[編集]

Kevin Buzzard は、数学者や数学科の学部生の間で Lean のような定理証明支援系を普及させることを目指す Xena プロジェクトを主導している。^[15]Xena プロジェクトの目標の1つは、インペリアル・カレッジ・ロンドンの学部生の数学カリキュラムにあるすべての定理と証明をLeanで書き直すことである。
2020年12月、数学者の Peter Scholze は自身の liquid vector space に関する定理を Lean で形式化することは可能かという挑戦状を Lean コミュニティに持ち込んだ。この挑戦は Liquid Tensor Experiment と呼ばれ、2022年7月に完了が宣言された。^[16]
フィールズ賞受賞者の Terence Tao は、2023年10月のSNSへの投稿で、自身の論文を Lean 4 で形式化する過程で小さな（しかし非自明な）ミスを見つけることができたと明かしている。^[17]
数学理論の形式化や自動証明に対する応用だけでなく，ソフトウェアの正しさの検証やセキュリティの方面でも Lean を使用した研究がなされている。AWS は，Cedar 言語の正しさとセキュリティ特性を保証するのに Lean を使用した。^[18]

脚注[編集]

^ “Lean Prover About Page”. 2023年7月7日閲覧。
^ Sebastian Ullrich (2023). An Extensible Theorem Proving Frontend. Karlsruhe Institute of Technology. "1.3.3 The Essence of Lean"
^ ^a ^b ^c Sebastian Ulrich (2023). “An Extensible Theorem Proving Frontend”. Karlsruhe Institute of Technology. "1.3.4 A Short History of Lean"
^ “Releases/v3.0.0”. GitHub. 2024年4月27日閲覧。
^ “Release v4.0.0-m1 leanprover/lean4”. GitHub. 2024年3月28日閲覧。
^ ^a ^b ^c Leonardo de Moura, Sebastian Ullrich (2021). “The Lean 4 Theorem Prover and Programming Language”. 28th International Conference on Automated Deduction (CADE-28).
^ “The Lean Mathematical Library”. mathlib community. 2024年3月25日閲覧。
^ “Mathlib porting status”. 2024年3月25日閲覧。
^ “Mission - Lean FRO”. Lean FRO. 2024年3月28日閲覧。
^ “Release v4.0.0 leanprover/lean4”. GitHub. 2024年3月28日閲覧。
^ ^a ^b “Tabled Typeclass Resolution”. arxiv. 2024年5月25日閲覧。
^ 型に応じて、同じ処理に複数の実装を提供すること
^ “An Abstract Machine for Tabled Execution of Fixed-Order Stratified Logic Programs”. ResearchGate. 2024年5月4日閲覧。
^ “‘do’ unchained: embracing local imperativity in a purely functional language (functional pearl)”. ACM. 2024年5月25日閲覧。
^ “What is the Xena project?”. Kevin Buzzard. 2024年4月27日閲覧。
^ “Completion of the Liquid Tensor Experiment”. leanprover community. 2024年4月10日閲覧。
^ “@tao@mathstodon.xyz”. mathstodon.xyz. 2024年4月10日閲覧。
^ “Lean Into Verified Software Development”. AWS. 2024年5月24日閲覧。

外部リンク[編集]

Lean Website Lean の公式サイト。
Lean 4 Web Lean のオンラインエディタ。
Reservoir Lean のパッケージレジストリ。パッケージをインデックスするだけでなく、ビルドとテストも行う。
vscode-lean4 VSCode に Lean 言語のサポートを追加する拡張機能。Unicode 記号をサポートしていて、× に対する \times のようなLaTeXに似たシーケンスを使用して入力ができるようにする。

[1] “Lean Prover About Page”. 2023年7月7日閲覧。

[2] Sebastian Ullrich (2023). An Extensible Theorem Proving Frontend. Karlsruhe Institute of Technology. "1.3.3 The Essence of Lean"

[:0-3] Sebastian Ulrich (2023). “An Extensible Theorem Proving Frontend”. Karlsruhe Institute of Technology. "1.3.4 A Short History of Lean"

[4] “Releases/v3.0.0”. GitHub. 2024年4月27日閲覧。

[5] “Release v4.0.0-m1 leanprover/lean4”. GitHub. 2024年3月28日閲覧。

[:1-6] Leonardo de Moura, Sebastian Ullrich (2021). “The Lean 4 Theorem Prover and Programming Language”. 28th International Conference on Automated Deduction (CADE-28).

[7] “The Lean Mathematical Library”. mathlib community. 2024年3月25日閲覧。

[8] “Mathlib porting status”. 2024年3月25日閲覧。

[9] “Mission - Lean FRO”. Lean FRO. 2024年3月28日閲覧。

[10] “Release v4.0.0 leanprover/lean4”. GitHub. 2024年3月28日閲覧。

[:2-11] “Tabled Typeclass Resolution”. arxiv. 2024年5月25日閲覧。

[12] 型に応じて、同じ処理に複数の実装を提供すること

[13] “An Abstract Machine for Tabled Execution of Fixed-Order Stratified Logic Programs”. ResearchGate. 2024年5月4日閲覧。

[14] “‘do’ unchained: embracing local imperativity in a purely functional language (functional pearl)”. ACM. 2024年5月25日閲覧。

[15] “What is the Xena project?”. Kevin Buzzard. 2024年4月27日閲覧。

[16] “Completion of the Liquid Tensor Experiment”. leanprover community. 2024年4月10日閲覧。

[17] “@tao@mathstodon.xyz”. mathstodon.xyz. 2024年4月10日閲覧。

[18] “Lean Into Verified Software Development”. AWS. 2024年5月24日閲覧。

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]