証明支援系Lean〈リーン〉は、かなり前（2017年くらい）から注目しているソフトウェアです。注目はしているんですが、ちゃんと調べる機会がなかったので、このブログで触れたことはありませんでした。2022年のうちに紹介したい（今は大晦日の夜）。
Leanは現在、バージョン3系とバージョン4系が混在しています。このため情報が錯綜していて、分かりにくい状況になっています。今はバージョン3系が使われていますが、これからLeanを使い始めるならバージョン4をインストールしてもいいかも知れません（ただし、開発バージョンであることは承知の上で）。
Leanは、CoqやIsabelleと同様、証明支援系〈proof assistant〉として設計開発されました。実際、機械可読な定理記述のために広く使われています。
バージョン4になりLeanは、汎用プログラミング言語としての機能・特性を前面に打ち出してきました。Lean4の What is Lean には次のように書いてあります。
Lean is a functional programming language that makes it easy to write correct and maintainable code.
Leanは、正しくて保守可能なコードを容易に書ける関数型プログラミング言語です。
まずはプログラミング言語なわけです。二文目に証明支援機能について書いてあります。
You can also use Lean as an interactive theorem prover.
Leanを対話的定理証明系として使うことも出来ます。
Lean 4が汎用プログラミング言語として普及すれば、歴史上はじめての「証明支援機能も備えた“実用的”汎用プログラミング言語」になるかも知れません。
内容：
Lean 3とLean 4
Leanは、2013年から開発が始まっているので、既に十年近い歴史を持ちます。しかし、著名な証明支援系である Coq、Isabelle は三十数年に渡り開発が継続しているので、証明支援系の世界ではLeanはまだ“若手”に分類されます。以下のリストは、2022年時点において、証明ソフトウェアと吉本興業の芸人さんを、デビューが古い順に並べたものです。
- Mizar / Andrzej Trybulec (1973～現役) 現役最古参の証明検証系、49年目
https://en.wikipedia.org/wiki/Mizar_system, http://mizar.uwb.edu.pl/ - 明石家さんま (1974～現役) 芸歴48年
- Isabelle / Lawrence Paulson (1986～現役) Coqと共に証明支援系のニ大巨頭、36年目
https://en.wikipedia.org/wiki/Isabelle_(proof_assistant), https://isabelle.in.tum.de/ - 木村祐一 (1986～現役) 芸歴36年
- Coq / Thierry Coquand, Gérard Huet (1989～現役) おそらく最も有名な証明支援系、33年目
https://en.wikipedia.org/wiki/Coq, https://coq.inria.fr/ - 千原兄弟 (1989～現役) 芸歴33年
- Agda / Ulf Norell, Catarina Coquand (2007～現役) 原則プログラミング言語だが、証明記述に使える、15年目
https://en.wikipedia.org/wiki/Agda_(programming_language), https://wiki.portal.chalmers.se/agda/pmwiki.php - Idris / Edwin Brady (2007～現役) Agda同様、プログラミング言語／証明記述可能、15年目
https://en.wikipedia.org/wiki/Idris_(programming_language), - ミルクボーイ (2007～現役) 芸歴15年
- Lean / Leonardo de Moura (2013～現役) 期待の新人、9年目
https://en.wikipedia.org/wiki/Lean_(proof_assistant), https://leanprover.github.io/ - 霜降り明星 (2013～現役) 芸歴9年 第七世代
Leanは、21世紀になって登場した証明支援系では最も成功したソフトウェアだと言っていいでしょう。そして、今後の進化発展も期待されています。
Lean 4は、2021年に最初にリリースされたLeanの最新バージョンです。それまでのLean 3とは大幅に変更されています。冒頭に述べたように、Lean 4は汎用プログラミング言語として自分を位置付けています。もちろん、証明支援機能を捨てたわけではなくて、証明支援系もパワーアップしています。
Lean 3はメンテナンス・フェーズに入り、コア開発チームはLean 4開発に専念しています。まだしばらくは、Lean 4に実験的機能が入ったり仕様の変更は続くでしょう。今現在はLean 3のほうが安心して使えますが、長期的には、Lean 3 → Lean 4 という移行が進んでいくでしょう。
Leanに関するオフィシャルな情報は、Lean 3もLean 4も https://leanprover.github.io/ の配下に存在します。Leanのバージョンを確認・意識しないと混乱してしまうので注意してください。
- Lean 3.3のマニュアル：https://leanprover.github.io/reference/
- Lean 4.0の文書： https://leanprover.github.io/documentation/
Lean 4の文書にはまだだいぶ欠け（未完成部分）があります。googleなどで「Lean」について検索すると、Lean 3の情報が引っかかることが多いでしょう。Lean 4にはまったく当てはまらない事もありますから鵜呑みにするのは危険です。
インストール
https://leanprover.github.io/lean4/doc/quickstart.html に、VSCode からのインストール方法が紹介されています。ここでは、Leanバージョンマネージャelan〈エラン〉からブートストラップする方法を紹介します。
elanのインストール方法は、https://github.com/leanprover/elan に書いてあります。bash が動く環境ならば、次のようにします。
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
インストール用のシェルスクリプトをダウンロードして、それを実行する方式です。Windowsでは、bashの代わりにpowershellを使った同様な方法でインストールできます（上記のページ参照）。
elanの情報も多くないのですが、elanは、Rust言語のrustupをLean用に書き換えたものなので、rustupに関する資料（例えば、https://rust-lang.github.io/rustup/）を参考に出来ます。elan, rustupは、「Rubyのrbenv」「Pythonのpyenv」「Node.jsのnvm」のような役割のソフトウェアです。
elanが使えるようになると、好きなバージョン（バージョン3でもよい）のLeanを ~/.elan/ *1の下にインストールできます。複数のバージョンのLeanをインストールして切り替えて使うこともできます。
elanでは、特定のバージョンのLean一式をツールチェーンと呼びます。ツールチェーンは、次のネーミングパターンにより命名されます。
- ツールチェーン名 ::= オリジン ':' ローカル名
- ローカル名 ::= バージョン | チャンネル名 ('-' 日付)?
オリジンは、githubのURLから、先頭の 'https://github.com/' を取り除いた名前です。次の2つのオリジンがあります。
- leanprover-community/lean -- lean 3の配布
- フルURL: https://github.com/leanprover-community/lean
- 2022年末の最新バージョンは 3.50.3
- leanprover/lean4 -- lean 4の配布
- フルURL: https://github.com/leanprover/lean4
- 2022年末の最新バージョンは 4.0.0-m5
チャンネルは stable と nightly の2つがあります。オリジンとバージョンまたはチャンネルを組み合わせて次のようなツールチェーン名が作れます（いずれも実在しています）。
- leanprover-community/lean:3.23.0 （バージョン指定）
- leanprover-community/lean:nightly （nightlyチャンネル）
- leanprover-community/lean:stable （stableチャンネル）
- leanprover/lean4:nightly （Lean 4のnightlyチャンネル）
- leanprover/lean4:nightly-2022-12-24 （チャンネルと日付指定）
バージョン、または日付指定のチャンネルにより特定のバージョン（gitコミット）を一意的に識別できます。チャンネルだけの指定は変動します。例えば、今日（2022年大晦日）の時点の leanprover-community/lean:stable は
leanprover-community/lean:3.50.3 ですが、しばらくすると leanprover-community/lean:3.50.4 になっているかも知れません。
オリジンなしの nightly, stable という名前も使えます。現在、nightly は version 3.9.0, nightly-2020-04-28 （何故か古い！）の別名で、 stable は version 3.50.3 の別名です。オリジン付きの長い名前を使っておいたほうが分かりやすいし無難だと思います。
現在インストールされているツールチェーンをリストするには、elan show または elan toolchain list を使います*2。
> elan toolchain list leanprover-community/lean:3.23.0 leanprover-community/lean:nightly leanprover-community/lean:stable leanprover/lean4:nightly (default) leanprover/lean4:nightly-2022-12-24 leanprover/lean4:stable
ツールチェーンのインストール／アップデートには、elan toolchain install または elan toolchain update を使います。elanでは、install と update は同じコマンドの別名です。
> elan toolchain update leanprover-community/lean:stable
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v3.50.3
info: downloading component 'lean'
863.4 KiB / 7.9 MiB ( 11 %) 0 B/s ETA: Unknown 5.7 MiB / 7.9 MiB ( 72 %) 863.4 KiB/s ETA: 3 s
7.9 MiB / 7.9 MiB (100 %) 2.9 MiB/s ETA: 0 s
info: installing component 'lean'
leanprover-community/lean:stable installed - Lean (version 3.50.3, commit 855e5b74e3a5, Release)
バージョン固定したいときは特定バージョンまたは日付指定チャンネルを使用、最新のバージョンを追いかけたいときはチャンネルだけ指定してインストール／アップデートします。elan自身のアップデートは elan self update で出来ます。
デフォルトで使うツールチェーンは、elan default で設定します*3。
> elan default leanprover/lean4:stable info: using existing install for 'leanprover/lean4:stable' info: default toolchain set to 'leanprover/lean4:stable' leanprover/lean4:stable unchanged - Lean (version 4.0.0, commit 7dbfaf9b7519, Release) > elan show installed toolchains -------------------- leanprover-community/lean:3.23.0 leanprover-community/lean:nightly leanprover-community/lean:stable leanprover/lean4:nightly leanprover/lean4:nightly-2022-12-24 leanprover/lean4:stable (default) active toolchain ---------------- leanprover/lean4:stable (default) Lean (version 4.0.0, commit 7dbfaf9b7519, Release)
バージョン3とバージョン4では互換性がないし、バージョン4のあいだでも互換性を破壊する変更がされる可能性があります。したがって、バージョンマネージャelanによるツールチェーン管理は必須です。
Leanプロジェクト
Leanプロジェクトのビルドツールやパッケージマネージャには、過去次のようなものがありました。
- leanmake
- leanproject
- leanpkg
Lean 4では、これらのツールはもはや使いません。代わりに lake〈レイク〉という統合ツールを使います。elan をインストールすれば lake は同梱されているので、別にインストールする必要はありません。
Lean 4のプロジェクトは、適切な構造を持ったディレクトリ〈フォルダ〉ですが、lake でプロジェクトの初期化が出来ます。
> mkdir my-lean-proj > cd my-lean-proj > lake init my-lean-proj
同じことを次のコマンドだけでもできます。
> lake new my-lean-proj
Leanプロジェクトは、gitリポジトリであることを要求しています。lake は git を呼び出して、git init も行います。git を事前に使える状態にしておく必要があります。lake は次のファイル・ディレクトリを作ります。
- .git/
- .gitignore
- MyLeanProj.lean
- lakefile.lean
- lean-toolchain
- Main.lean
Leanでは、プロジェクトとパッケージの区别はありません。プロジェクトディレクトリのスナップショットであるgitコミットがパッケージとして共有や配布の対象になります。
Lean 3では、leanpkg.toml というメタデータ・ファイルがありましたが、Lean 4では廃止されました。Lean 4におけるプロジェクト・メタデータは、lean-toolchain, lakefile.lean に書き込まれています。lean-toolchain は1行のテキストファイルで、elanが管理するツールチェーン名が書かれています。lakefile.lean には、その他のメタデータやビルドの設定、他のパッケージへの依存性などを書きます。
MyLeanProj.lean と Main.lean は、サンプルの“Hello, world! プログラム”です。lake build とすると、./build/bin/ の下にネイティブ実行ファイルが作られます。Lean 4は、LLVMインフラストラクチャ上に構築された言語処理系で、中間でC言語ソースを吐き出して、LLVM clang コンパイラを使ってネイティブ実行ファイルを生成します。Leanツールチェーンに clang も含まれるので、Cコンパイラを別に準備する必要はありません。
Lean 3以前と同様に、Lean仮想機械〈バイトコード・インタプリタ〉上でのプログラム実行もサポートしています。ネイティブコードと仮想機械コードを混ぜた実行も可能なようです。
Leanパッケージ
前節で述べたように、Leanのパッケージは、Leanプロジェクトディレクトリのスナップショットです。gitリポジトリのブランチ名やタグ名、コミットオブジェクトのハッシュ値などでLeanパッケージは識別されます。
Node.js の https://www.npmjs.com/ や、Rust言語の https://crates.io/ のような、パッケージを集約して管理するレジストリは存在しません。gitリポジトリのURLを直接指定して、他のパッケージを自分のプロジェクトに取り込みます。
例えば、Lean 4の数学ライブラリmathlib4は、https://github.com/leanprover-community/mathlib4.git というURLで公開されています。このライブラリを自分のプロジェクトで利用するには、lakefile.lean に次の1行を書きます。
require mathlib from git "https://github.com/leanprover-community/mathlib4.git"
バージョン（gitコミット）を固定したいときは、コミットのハッシュ値〈オブジェクトID〉を付けます。
require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "9efcb9508435caeb4281b14455f37b88f8ffc2e5"
アットマークの後にブランチ名（例："main"）やタグ名（例： "snapshot-2019-10"）を書くこともできます。
依存性を記述するrequire文を書き足したら、lake update します。
> lake update cloning https://github.com/leanprover-community/mathlib4.git to .\lake-packages\mathlib cloning https://github.com/xubaiw/CMark.lean to .\.\lake-packages\CMark cloning https://github.com/leanprover/lake to .\.\lake-packages\lake cloning https://github.com/leanprover/doc-gen4 to .\.\lake-packages\doc-gen4 cloning https://github.com/mhuisi/lean4-cli to .\.\lake-packages\Cli cloning https://github.com/gebner/quote4 to .\.\lake-packages\Qq cloning https://github.com/gebner/aesop to .\.\lake-packages\aesop cloning https://github.com/hargonix/LeanInk to .\.\lake-packages\leanInk cloning https://github.com/xubaiw/Unicode.lean to .\.\lake-packages\Unicode cloning https://github.com/leanprover/std4 to .\.\lake-packages\std
プロジェクトディレクトリの ./lake-packages/ 以下にパッケージ（gitリポジトリ）がクローンされます。実際にインストール〈クローン〉されたgitコミットは、./lake-manifest.json に記録されます（npmの package-lock.json のようなもの）。インストールされたパッケージの内容は、import文で利用可能となります。
エディタ
Leanには、LSP〈Language Server Protocol〉サーバーが付属しているので、LSP対応エディタならLeanコードの編集作成ができます。（テキストファイルを作れればいいので、素のテキストエディタでもLeanコードは書けますが、まったく現実的ではないです。）
LSP対応エディタのなかでも、Leanプログラミングに関して手厚いサポートを受けられるのは VSCode です。拡張機能 lean4（https://marketplace.visualstudio.com/items?itemName=leanprover.lean4）をインストールすれば、充実したLean 4開発環境が手に入ります。
オンラインで利用できるWebエディタ https://leanprover-community.github.io/lean-web-editor/ はよくできたLeanエディタで、インストールなしで使えます。しかし残念ながら、現状はLean 3しかサポートしてないようです。
#eval lean.version -- (3, (50, 3))
おわりに
現時点で、Lean 4を汎用プログラミング言語として使えるか？ と言うと、それはNOです。パッケージ／ライブラリがまったく足りてません。たいていの言語が備えているライブラリ機能、例えば、HTTPサーバー／クライアント、JSONやXMLの処理、データベースへの接続などが揃っていません。どこかの誰かが既にライブラリコードを書いているかも知れませんが、パッケージレジストリがないのでライブラリコードを効果的に探すことができません。
[追記]https://github.com/leanprover/lean4/tree/master/src/Lean/Data の下に、「JSONやXMLの処理」のコードを見つけました。が、ソースツリーを辿っているときにたまたま見つけたものです。[/追記]
Lean 4がLLVMベースであることから、他言語で書かれたライブラリを取り込むことが比較的容易で、それほど遠くない将来にライブラリが揃ってくることが期待できます。しかし、今はライブラリがありません。
証明支援系として考えると、Lean 3から蓄積されている膨大な定理ライブラリ mathlib が存在し、Lean 4へのポーティングも進んでいます。すぐに使える定理記述もあります（https://github.com/leanprover-community/mathlib4/ 参照）。
これらの事情を考えると、当面のLean 4の利用法は「証明支援機能を備えた汎用プログラミング言語」というより、「プログラミングもできる証明支援系」ということになるでしょう。
