Lean は Calculus of Inductive Constructions (CIC) と呼ばれる型システムに基づく、純粋関数型プログラミング言語である。 functional but in-place と呼ばれるプログラミングパラダイムに基づいており、従来の純粋関数型言語のパフォーマンス上の欠点を改善している。さらに、Lean は衛生的かつ非常に強力なメタプログラミングフレームワークを備えており、ユーザがパーサやエラボレータを自在に拡張することができる。Lean はまた、プログラミング言語であると同時に証明支援系(theorem prover)でもあり、Mathlib という大規模な形式化された数学ライブラリを擁する。

## 歴史

### 2013年: 開発開始

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

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 で削除されることになる。

### 2015年: Lean 2

2015 年、Lean の最初の公式リリースである Lean 2 が発表された。帰納型の適切なサポートや組み込みタクティクの拡張など、欠けていた重要な機能が追加されたほか、主要な機能として Lean 2 ではホモトピー型理論 (HoTT) のサポートが追加された。

### 2017年: Lean 3

最初にリリースされた比較的安定したバージョンは Lean 3 で、2017年の1月20日にリリースされた。Lean 3 では、あまり使用されていなかった Lua による構文拡張機能が削除され、根本的に異なるアプローチが採用された。Lean 自体がプログラミング言語とされ、Lean 自体によりタクティクの定義やそのほかのメタプログラミングが可能になった。Lean 2 からのもう一つの大きな変更は、ホモトピー型理論 (HoTT) のサポートの廃止である。HoTT のサポートが廃止された理由としては、

- 証明無関係(proof irrelevance) の公理がないと、タクティクを効率的に実装するのが難しくなり、コードの重複が生じるという問題
- 当時 「book HoTT」と最近の計算的な Cubical Type Theory のどちらが望ましいか不明だったという問題

が挙げられる。また、Lean で数学を形式化するライブラリである mathlib がコミュニティ管理の 独立したプロジェクトとして分離された。

バージョン3.4.2以降、Lean 3の開発は正式に終了し、Lean 4の開発が始まった。

### 2021年: Lean 4

2021年、Lean 4の最初のマイルストーンリリースが発表された。C++ではなく Lean 自身によって再実装され、「Lean は定理証明支援系であると同時に、汎用プログラミング言語でもある」と標榜するようになった。

Lean 4 より以前のバージョンでは、次のような問題点が認識されていたが、Lean 4 では大幅に改善された。

- Lean 3 での経験から、定理証明を上手く行うためにはメタプログラミングフレームワークを備え、高い拡張性を有することが重要であると認識されていた。しかし Lean 3 のシステムの多くの部分が、C++ で書かれた Lean 3 のソースコードを変更しない限り、ユーザには変更できなかった。
- Lean 3 メタプログラミングは仮想マシン解釈のオーバーヘッドにより非効率だった。これにより Lean 3 での自動証明は、C++ や OCaml のような効率的なコンパイラを持つ言語で実装された同様の自動証明とは競合できなかった。

Lean 4 は完全に拡張可能であり、パーサ、エラボレータ、タクティク、決定手続き(decision procedure)、プリティプリンタ、コードジェネレータを変更・拡張することができる。また Lean 4 は対話的証明のためにカスタマイズされた衛生的なマクロ(hygienic macro)を持つ。Lean の構文をユーザが改変する際に C++ コードに触れる必要はなくなった。

さらに Lean 4 ではメモリ管理手続きが改善されたほか、テーブル解決に基づく新しい型クラス解決アルゴリズムが使用され、パフォーマンスが改善された。また、Lean 4 は functional but in-place と呼ばれる新しいプログラミングパラダイムに基づくようになった。

Lean 4 には Lean 3 との後方互換性はない。Lean3 で開発されていた主要なライブラリとして、2017年ごろから開発が行われていたmathlib が挙げられるが、コミュニティにより Lean4 への書き直しが行われた。これには100万行以上のコードを書き換える必要があったが、この移行作業は2023年7月に完了した。

### 2023年: Lean FRO設立

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

## Leanの型システム

### 無矛盾性

非形式的な数学において一般的に基礎理論として採用されているのは ZFC 集合論と呼ばれる理論であるが、Lean で採用されている基礎理論は Calculus of Inductive Constructions (省略して CIC と呼ばれる) であって、これとは異なる。

Lean の型システムの無矛盾性については、Lean 3 の時代の結果として、「$ZFC_{\omega }$が無矛盾であることと、 $Lean_{\omega }$ が無矛盾であることが同値であること」が知られている。ただし $ZFC_{\omega }$ とは、「ZFC に、任意の有限個の到達不能基数が存在するという仮定を足したもの」を指し、 $Lean_{\omega }$ とは「Lean 3の型システムに、任意の有限個の universe があるという仮定を足したもの」を指すものとする。 これは、ZFC の中で Lean 3 のモデルが構築でき、Lean 3 の中で ZFC が構築できるためである。

Lean 4 については、入れ子帰納型 (nested inductive type) や構造体のη変換 (η for structures) が導入されたことが型システムに大きな影響を及ぼしており、Lean 3 に対する無矛盾性の証明はそのまま適用できなくなった。

### 型付けの一意性

Lean では項の型は一意である。つまり、項 e の型が α であり同時に β であるとき、α と β は(どこかの型宇宙において)等しい。

なお、これは「型とは、集合のようなもの」という、型に対する素朴な理解とは矛盾することに注意が必要である。集合の場合は、$U\subseteq V$ かつ $x\in U$ であるならば、$x\in V$ が成り立つ。しかし、Lean では型 U の項を他の型の項であると直接見なすことはできない。

### Coqとの差異

旧Coq (現在のRocq) は、Lean と同じくCalculus of Inductive Constructions (CIC) を採用しているという点で、Lean とよく似ているが、以下のような点で異なる。

- Lean では定義は宇宙多相(universe polymorphic) であることができる。つまり、一つの定義ですべての宇宙レベルを賄うことができる。しかし、Coq では定義は不定宇宙(indefinite universe)に棲んでいる。つまり、それぞれの定義は特定の宇宙に棲んでいるが、その宇宙レベルはグローバルに可変になっている。
- Coq では余帰納型(coinductive type)がサポートされているが、v4.16.0 の時点で Lean 4 は coinductive type をサポートしていない。
- Lean では証明無関係(proof irrelevance)を definitional equality としてサポートしているが、Coq では propositional equality としてこれを主張する公理が用意されている。

## Lean の機能

### 対話的実行

プログラミング言語としての Lean は、関数などの式を部分的に実行して評価することが容易にできるように設計されている。`#eval` というコマンドが存在し,関数などをその場で評価することができる。いわば、Jupyter Notebook のような対話的な実行環境が最初から利用可能であるということができる。

### フィールド記法

Lean はオブジェクト指向言語ではなく、オブジェクトやクラスに相当する概念は存在しないが、関数適用を「まるでフィールドにアクセスするかのように」書くことができる記法が用意されている。これは Nim 言語における Uniform Function Call Syntax に似ている。

### 正格評価

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

### 帰納型

Leanでは帰納型を定義することができる。帰納型とは、「その型の項を得る関数(コンストラクタ)」を有限通り指定することで定まる型であり、Leanでは「その型の上の関数/述語を得る方法(再帰原理)」が同時に生成されることで帰納法が可能であることが保証される。

帰納型の最も簡単な例は、列挙型である。列挙型とはある定められた有限通りの値しか取らない型のことで、たとえばBoolはLeanの標準ライブラリで列挙型として定義されている。列挙型は、「コンストラクタが引数を取らない」という特別なケースの帰納型である。

コンストラクタは引数をとっても構わない。特にこれから定義しようとしている自分自身を引数に取ることも許されるので、再帰的なデータ型を定義することができる。再帰的な帰納型の最も簡単な例は、自然数である。自然数はLeanの標準ライブラリでは次のように定義されている。

この定義はペアノの公理に基づいており、すべての自然数はゼロもしくは他の自然数の後者であると述べている。ペアノの公理には「コンストラクタが単射」「コンストラクタの像が重ならないこと」「帰納法の原理」も含まれるが、それらの成立はLeanによって自動的に保証される。
自然数の加算はパターン・マッチングを使用して、再帰的に定義できる。

### 証明

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

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

Lean の機能として、タクティクによって証明項を構成することができる。`by` キーワードによってタクティクモードに入ることができる。タクティクモードの中では、「現在利用できる仮定や命題」「今示すべきこと」が常に infoview に表示され、対話的に証明を書くことができる。

### 依存型

Lean は依存型を持つ。つまり、関数 `f : A → B` があったときに、`f` による `t : A` の返り値 `f t` の型が `t` に依存していてもよい。このとき `f` の型を `f : (t : A) → B` のように表記する。これにより、命題に正しく型を付けることが可能である。

依存型がなければ命題(これは一種の型である)が項に依存することができないので、表現することができる命題の範囲がとても狭まってしまう。定理証明支援系をプログラミング言語として実現するうえで、依存型があることはとても重要な役割を果たす。
また、依存型はより柔軟にプログラムに型を付けることを可能にし、型で表現できるソフトウェアの仕様の範囲を広げる。以下は「長さが `n` であるようなリスト」を `Subtype` として表現する型である。

### 拡張可能性

Lean は強力なメタプログラミング機能を持っており、新しい記法の定義や証明の自動化が行えるようになっている。以下は、`notation` コマンドで記法を定義する例である。

`declare_syntax_cat` コマンドや `macro_rules` コマンドを使うことで、さらに複雑な構文も定義することができる。

### 自動証明

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

また次は、直観主義論理(排中律を仮定しない論理)における証明を自動で行ってくれるタクティクの例である。

## Lean の特徴

Agda や Coq, Isabelle などの他の定理証明支援系と比べると Lean にはどのような特徴があるだろうか。この中で Isabelle は依存型がなく、依拠している基礎が異なるという著しい差異がある。Agda と Coq と比較すると、基礎はほぼ同じであるが、Lean には以下のような特徴がある。

### テーブル化型クラス解決(Tabled Typeclass Resolution)

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

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

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

### 拡張された do 記法

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

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

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

たとえば、以下は Lean 4 で実装したエラトステネスの篩である。

### Functional but in-place

ほとんどの関数型言語は、メモリ管理を自動で行うためにガベージ・コレクタを利用している。一方で、各値の正確な参照カウントを保持することで、破壊的更新などの最適化が可能になる。Lean は、純粋な関数型言語でありながら参照カウントを利用してメモリ管理を行う。参照カウントがちょうど1の値(つまり共有されていない値)を更新するとき、自動的に破壊的更新が行われる。このことを指して、Lean のプログラミングパラダイムのことを functional but in-place (FBIP) と呼ぶ。特に、Lean で配列のようなデータ構造を扱うとき、FBIP によりコードの純粋性を保ちながら効率的なコードを生成することが可能である。

これにより Lean のコンパイラが生成するコードは効率的になり、 他の静的型付け言語と比較しても遜色のないものになった。

実際に Lean が値の破壊的変更を行っていることは、次のようなコードで確認することができる。

### 衛生的でありながら強力なメタプログラミングフレームワーク

ITP(対話的定理証明支援系)において、構文を拡張可能にすることは複雑な数学的対象をわかりやすく表現するのに重要であるのみならず、ライブラリ開発においても再利用可能な抽象化を行うために役立つ。このように表現力の高いマクロシステムを持つことは ITP にとって極めて重要なのだが、Lean 3 のものを含め既存の ITP のマクロシステムには問題があった。

問題点は主に以下の2点である:

- マクロの抽象化が弱く、しばしば冗長な定義をせざるをえなかった。
- タクティクを定義する際などに、マクロ展開において名前の偶発的な衝突が起こってバグを生み出していた。

Lean 4 はこれらの問題を Scheme ファミリーに着想を得た新しいマクロシステムを開発することにより同時に解決した。新しいマクロシステムは、複数のマクロ抽象化レベルを単一で統一的なシステムで実装することを可能にし、高い表現力と安全性を両立した。

たとえば、以下は Coq のライブラリ math-comp における和のΣ記号の定義である。見てわかるように少しずつ異なる同様の定義が 12 回繰り返されている。

ほぼ同じことが Lean の数学ライブラリ mathlib4 では次のように表現されている。明らかに繰り返しが少なく、簡潔な書き方になっていることがわかるだろう。

これは Lean では `syntax` および `declare_syntax_cat` というコマンドが用意されていることと関係がある。Lean ではユーザが構文カテゴリを定義し、パーサの拡張を抽象化された高水準言語で行うことができる。これは Lean 3 までの静的なマクロでは不可能だった。

## 利用

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