定理証明支援系Leanのインストールと初期設定(Linux)

※そろそろLean 4が出そうなのでここの情報ももはや正確ではないと思います(2021/09/11)。

 

Leanのドキュメントは原則としてLean communityからたどれます。Lean自体のホームページからインストール方法を探そうとするとここに飛ばされます。

僕が使っているLinuxDebian/Ubuntuですが、せっかくなのでGeneric Linuxのほうをやってみます(Debian/Ubuntuのほうに掲載されているシェルスクリプトを読んでみてもGeneric Linuxと同じようなことをやっている)。

というわけで

curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh

を実行します。
   default toolchain: stable
modify PATH variable: yes

でよいか聞かれます。普通はこれでいいと思うのでエンターを押して先に進みます。しばらくするとインストールが終わります。

再起動とかsource ~.profileするとちゃんとPATHに$HOME/.elan/binが入っているのがわかります。Leanの本体は$HOME/.elan/toolchains/stableにあります。

新しいバージョンを入れるときは、

elan toolchain install leanprover/lean4:v4.0.0-m2
をするか、leanpkg.tomlに

lean_version = "leanprover/lean4:v4.0.0-m2"

って書けば自動で入ると思います。(elan updateもあり?)


Leanのサイトに戻りましょう。VSCodeはいいと思うので(leanにパスが通っていれば問題なく動くと思います)、次はleanprojectをインストールします。まあこれも書いてあるとおりなんですが…ページ上のほうにpython3-pipとpython3-venvを入れろと書いてありますのでそれは事前にやっておきましょう。入ってなくても途中でやることにはなります。
で、これでインストール自体は終わりなのですが、ページの最後を見ると新規プロジェクトの作り方(leanprojectの使い方)へのリンクが載っています。プロジェクトを作ってからじゃないとVSCodeとかでも警告されるので、ここも読みましょう。ちなみにleanprojectを使うには事前にgitをインストールしておく必要があります。
どこかのフォルダでleanproject new my_projectとか入力すると、mathlibというleanの標準ライブラリ的なものがダウンロードされ、プロジェクトができます。(ダウンロードされない場合は先にleanproject get-mathlib-cacheをやっておくとうまくいくかも?

my_project/_target/deps/mathlib/srcを見ると線形代数・論理学などの様々な分野の定義・定理を含んだleanファイルがたくさんあるのがわかります。VSCodeでmy_projectフォルダを開き、公式サイトにしたがってtest.leanを作るついでにそっちも眺めてみるといいでしょう。
なお、リファレンスマニュアルのほうを読むとleanpkgコマンドを使うやりかたが最初に書いてあります。leanpkg new my_projectとするとmathlibの入っていない必要最小限の新規プロジェクトができるように見えます。
leanpkgとleanprojectの違いなどはよくわからないのですが、Leanは全体的に情報が錯綜しているのでそこは諦めましょう(leanpkgはgithub上でアーカイブされているので古い?leanpkgはleanの一部になっているようです(Lean4のリポジトリにもあります)。Using leanprojectによるとleanprojectはLean3までしかサポートしないようなのでleanpkgのほうが新しいようです)。
以上で環境構築は終わりなので、Learning Leanに列挙されているドキュメントを読んで、Leanを使ってみましょう。普通はTheorem Proving in Leanから入ればいいかと思いますが、途中で出てくる論理学・型理論の知識にあまりにも馴染みがない人は他のものを試してみてもいいでしょう。Mathematics in LeanやLogic and Proofなどでしょうか。ただLogic and Proofあたりの知識は他の本とか読んだほうがいい気もします。
僕自身は、どれか一冊を読んで身につけたというよりは、色々な場所でちょっとずつ触れて挫折しながら本当に基礎的な部分だけはわかってきたという感じなので日本語の本のおすすめとかはあまりできないのですが…いちおう挙げておくと、『数学基礎論講義』(田中一之ほか)は、ゲーデル不完全性定理のちょっと前くらいまで読んだ気がします。あと『数理論理学』(戸次大介)も日本語が上手ですごいと思いました。ただ、カリーハワード同型とか型システムの話を定理証明の文脈で書いた日本語の本は(というか英語の本も)あんまり知らないです。Coqについての入門書『Coq/SSReflect/MathCompによる定理証明』が最近出たのでそれくらいでしょうか…カリーハワード同型やCalculus of Constructionについては、Lectures on the Curry-Howard Isomorphismを読むといいのかもしれません。僕はほんのちょっとだけ読んだことがあります。

いずれにしろTheorem Proving in Leanを読むのは具体例が貧弱だったりして結構大変でした。これからもっと読みやすいのができるといいなと思います。