定理証明支援系Lean

Leanは、比較的新しい定理証明支援系（Lean以外にはCoqやIsabelleなどがある）である。

概要

学術研究用なのもあって特にメジャーバージョンアップでは大きな破壊的変化がある。

Lean2以前はよく調べていないがLean2にはHoTTサポートがあって3で無くなったらしい。3→4ではマクロシステムが刷新されたり、Leanの処理系のうちLean自体で書かれた部分がさらに増えたり？した。

Lean3

公式（githubでの名前はleanprover）と、半分公式みたいなコミュニティ（githubでの名前はleanprover-community）があって、公式では3.4.2まででアーカイブされているLean3もコミュニティversionでは3.47.0くらいになっている。また様々な分野の証明を集めたライブラリのmathlibもコミュニティの成果物である。

もうほとんど使われていないだろう。

Lean4

Lean4は現在のところ「公式」のみで扱われている。手元では、WindowsとMacではしばらく動かなかったが、2022年9月中旬頃にelanが1.4.2になったタイミングで動くようになった。しかしVSCode拡張は大文字/小文字の区別をうまく扱えずGo to definitionが失敗する（大文字/小文字の区別があるファイルシステムではおそらく問題なし？？）。既知のバグ。やなど。

VSCodeでの体感でもチェッカがLean3より明らかに速くなった。

学習用リソース

Lean3

https://leanprover-community.github.io/learn.htmlにリストされている。

最も基本的な使い方の解説がTheorem Proving in Leanであり、Leanを使って定理証明をする方法の概略が掲載されている。とりあえずはこれを読んでいけばいい。比較的よくまとまった資料であるが、Curry-Howard同型についてなど、型理論や証明論の事前知識が多少はないと読むのはやや大変かもしれない。そのあたりの知識から解説しているものもいちおう上記の一覧にある。

各tacticの動作など、辞書的な説明はreference manualに載っている場合もあるが、こちらは未完成である。

Programming in leanというのもあるが、これも少なくとも最近はあまりメンテナンスされていない。

Programming in leanに関する詳細

これまた未完成ではあるがProgramming in Lean — Programming in Lean 3.4.2 documentationを見ると説明が載っているかもしれない。programming in leanで検索すると、

https://leanprover.github.io/programming_in_lean/programming_in_lean.pdf

https://leanprover.github.io/programming_in_lean/

（この2つは同じ内容）

も出てくるが、こちらはリポジトリ(avigad/programming_in_lean)と比較すると古いバージョンのようである（リポジトリの”old”フォルダの内容に対応している）。

Lean4

前述の各資料に対応してhttps://leanprover.github.io/theorem_proving_in_lean4/title_page.htmlとhttps://leanprover.github.io/lean4/doc/とFunctional Programming in Leanがある。

Publications

日本語情報

定理証明支援系Leanのインストールと初期設定（Linux）（自分で書いたが、古いのでもう読まなくていい）

定理証明支援系 LEAN のインストール

Theorem Prover Leanの紹介 - Just $ A sandbox

定理証明リンク集

くらい。あんまりないが、順調にいけば今後増えていきそうではある。

2025/6追記最近はもっと増えてそう

metaprogramming関連

Leanの証明記述用言語（tactic）は、Leanそれ自体の上で実装されている。バージョン3→4によってさらにその傾向が強まりそうである。

tacticはmonadicな関数として実装されている。tacticをmonadで表現するというのはCoq用のMtac[^ziliani2013Mtac]などでも採用された手法である。

Lean3での例

筆者は研究活動の一環として、Lean 3のソースコード上に構造的に関連付けられた形でコメントを書けるようにするライブラリであるNtac（https://github.com/ge9/ntac）を公開している。これはLean 3のmetaprogrammingを活かした例である。

metaprogrammingについてはコミュニティのLearning resourcesの”Metaprogramming and tactic writing”の項目やhttps://leanprover.github.io/papers/tactic.pdfを参考にした。また、独自のtacticシステムを作成するためのガイドとして、https://leanprover-community.github.io/archive/stream/113488-general/topic/no.20lean.20messages.20output.20in.20hacked.20mode.htmlに実装上のヒントを得た。

基本的には、tacticという名前でStateモナドが定義されていて、各tacticはこのモナド値を返す関数として定義されている。しかしtacticは現在の状態しか持っておらず、コメントを紐づけたりするには証明の過程まで含めた全体の構造が欲しい。そこでntacでは、tacticの定義を変更して証明の「履歴」を木構造として保持するようにしたntacというモナドを定義し、既存のtacticを（適切な）ntacモナド値を持つような定義に変更した。

Lean4

Schemeを参考に、強力な衛生的（hygienic）マクロシステムが実装された。柔軟なNotationの定義ができるようになる。論文としては[^ullrich2020Notations]に詳しく書いてある。

上記「ntac」のLean4版は現在開発中。構文解析中に外部のプログラムを呼び出すなど、なんでもできて面白い。

例

replしてる例らしい https://github.com/leanprover-community/repl

tacticの移行とか

Lean3までの証明（のうちtacticで書かれたもの）をLean4に移植する方法について。
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Tactic.20porting.20assignments/near/296694161

とりあえず error_private_page で基礎知識を得るのがよさそう？

elan

leanを管理（各バージョンのインストール/アンインストールなど）するためのツール
適当にフォルダだけ消すとtoolchainの再インストールで引っ掛かるので、update-hashesも消すとよいかも
rustupのforkらしい関数型言語”兼”定理証明支援系Leanの環境構築

Lean3

https://leanprover-community.github.io/get_started.html を読む。elanってやつが入れば大丈夫で、mathlib-toolsとかleanprojectは（今はもう案内ないか？）無視でいい（後述）

パッケージ

Leanでの開発はまずパッケージを作るところから始まる。

leanpkg.tomlっていうメインの管理ファイルがあって、ここにLeanのバージョンとかを指定しておくと、無ければ（VS Codeでフォルダ開くタイミングとかで）自動でelanが取ってきてくれる

特定パッケージと、そのパッケージに依存するパッケージの双方を依存関係として指定したとして、バージョンの齟齬があったら何が起きるのかは不明である。ちなみにLean4の話だが、mathlib4に関してはhttps://github.com/leanprover-community/mathlib4に「If your project depends on std4 or quote4, let mathlib4 pull them transitively. That is, don't require them on your lakefile.lean」と明記されている。

mathlib

パッケージの一つ。半分標準のライブラリみたいなもの。数学の定理やリスト処理のプログラムなど、色々なものが形式化されている。文字列処理とかの便利関数も入ってるのでとりあえず入れて損はない

https://leanprover-community.github.io/mathlib-overview.html

mathlibの指定

leanpkg.tomlで

mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "lean-3.49.1"}

のように指定しておくと

leanpkg upgrade

でlean-3.49.1ブランチを取ってきてくれる。masterブランチ指定とかするとバージョンアップで互換性がなくなって困るのでこれがおすすめ。

mathlib-toolsとleanprojectについて

基本Lean3用なのでもう使われないかも

leanprojectはmathlib-toolsの一部で、mathlibをうまく扱うのが目的っぽい。python3 -m pip install mathlibtoolsで入る

prebuiltされた（ちなみに自前でビルドすると数時間かかる）mathlibを

https://oleanstorage.azureedge.net/mathlib/xxxxxxxxxxxxxxxxxxxxxxxxxxxxxx.tar.xz

（xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxはコミットID）からダウンロードして、oleanにtouchして最新版にしてくれるが、それだけの機能しかなく、動作もあまり分かりやすくない。しかもよくわからんが、Lean4には未対応っぽい（というか、mathlibというのはLean3のパッケージの名前なのでそれはそうか（Lean4用のmathlibはmathlib4））。このまま使われなくなりそう。

そこで、自分でそれをやるスクリプトを書いてpathに登録した。これで十分と感じる。

#!/bin/sh
if ! cd ../../../_target/deps/mathlib ;then
echo "must be run in 'mathlib' folders.  exiting."; exit
fi
find src -name "*.olean" | xargs rm
curl -o olean.tar.xz https://oleanstorage.azureedge.net/mathlib/`cat .git/HEAD`.tar.xz
#touch all .olean (this is also done by leanproject in mathlib-tools)
find src -name "*.olean" | xargs touch
if tar xvf olean.tar.xz ; then
rm -f olean.tar.xz
fi

new-oleans.sh

Lean4

初期設定

elanをまず入れてそれからLeanを、ってのがv3以前のやり方だったと思うがSetting Up Lean - Lean Manualによるとどうやらv4はVS Code拡張経由で入れられるようである。

パッケージ(lake)

lake new フォルダ名（この中にパッケージができる）、またはlake init パッケージ名（パッケージはカレントディレクトリに作成される）を実行。詳しいやり方はhttps://github.com/leanprover-community/mathlib4 とか。

lakeのドキュメントはここ https://github.com/leanprover/lean4/tree/master/src/lake

dependencyの書き方は https://github.com/leanprover-community/mathlib4/blob/master/lakefile.lean とかを参考に。stdのURLがここにある。

mathlib4

prebuiltされたものの提供はないっぽい。https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.9C.94.20use.20prebuilt.20release.3F

いや、https://github.com/leanprover-community/mathlib4を読むと、lake exe cache getで取ってこれるように最近なった？

そのかわりlake build Mathlibと打てば（lean3のmathlibに比べて）割とすぐにビルドが終わる（5分前後？）

require ml4 from git "https://github.com/leanprover-community/mathlib4" @ "master"

↑依存パッケージとしてはこういうふうに書くが、lake build ml4ではなくlake build Mathlibが正しいっぽい。

そもそも、require ml4じゃなくてrequire mathlibと必ず書かなきゃいけない説もある