Microsoftが開発したTheorem Prover Leanを紹介します.

特徴

他の言語と軽く比較する.
あくまで個人的な感想です.

	Lean	Coq*1	Agda	Isabelle
証明の書き方	structured proof, tactic, 函数定義	tactic	函数定義	structured proof, tactic
開発環境	emacs	emacs, CoqIDE	emacs	jEdit
ドキュメント	×	◎	○	△
implicit parameter	○	○	△	(型を使わないので不要)
Equational Reasoning	○(builtinなものはOK. 独自演算子は条件付き)	？(知らない)	◎	○(基本的にbuiltinなもののみサポート)
自動証明	×(なし？)	○(auto, omegaなど)	△(emacsのautoコマンド)	◎(auto, force, sledgehammerなど)
ライブラリ	◎	○？	△	○
パフォーマンス	○？	？(知らない)	×	○

証明の書き方

なんとstructured proof(上から下向きに書ける), tactic, 函数定義の全ての書き方をサポートしている.
他の言語から入ってきた人にも優しい仕様.

開発環境

インストールはバイナリがあるのでそれを入れるだけ.
インストールするとleanemacsというアプリケーションが使えるようになる.
leanemacsではリアルタイムチェッカーが走るし, エラーメッセージも見やすいので(emacsが嫌いじゃなければ)そんなに悪くないと思う.

ドキュメント

公式サイトにTutorialとかがある.
HTML版はブラウザ上でLeanを動かすこともできてすごい.

しかしドキュメントらしきものはこのtutorial.pdfくらいしかなく, より詳細な情報でまとまった文章はおそらく存在しない.
Leanを本格的に使うならここが一番問題.

implicit parameter

カリーハワード対応を使って証明を書くような言語では, implicit parameterが使えるのは結構重要.
Coqは割と優秀と聞く一方で, Agdaは少し省略するとしょっちゅう警告ばかり出す.

ここに関してはLeanもそれなりに優秀で, たくさん省略してもエラーになったり警告が出たりはしない.

Equational Reasoning

独自演算子に対してのReasoningは, それがグローバルに定義された演算子なら, refl attributeなどを対応する命題に付与することで使えるようになる.
ただしstructure(データ型を定義するときに使う)内の演算子に対しては使えないなどの制約があるらしい.
同値関係を含む構造を定義して, それに対するreasoningを書くことが出来ないので微妙に不便.

ちなみに, reasoningはsubst(a == b & ==> P a == P bなど)を自動でやってくれるようで, 実はこれのおかげでLeanでreasoningをすると非常に証明が楽になる.
a == bを指定すると, aの部分を現在のGoalの左辺から探して代入する操作をやってくれるのでこちらでsubstを指定する必要がない.
Leanの目玉機能の一つ.

自動証明

~~ドキュメントにも書いてないから多分ないです.~~

追記:
どうもblastがそれに当たるらしい.
blast派生のコマンドがいくつかあって, 代表的なものとしてsimp(simp attributeがついた定理を適用する), rec_simp(帰納法が使える？)などがある.

ライブラリ

(駆け出しの言語にしては)標準で結構色々なものが揃っている.
HoTTライブラリが用意されているあたりもポイント.
拡張子 .hleanがそれ.

ところで, 現在LeanファイルをHTMLやpdfファイルに変換するツールなどはない.
ので.leanファイルを直接見る以外に証明を読む方法がないので(ファイルの依存関係がややこしい場合は特に)結構不便.

パフォーマンス

ちょっと書いた限り重くなったりする気配はあんまりない.
リアルタイムチェッカーが走っている割には軽くて快適. (ここでAgdaの方をチラ見する)

所感

色んな書き方ができるのは, 参入コストが下がると考えれば悪いことではないと思う.
Equational Reasoningでsubstを指定しなくていいのは予想以上に楽だったので, 普段苦労している人はこれだけでも触ってみる価値はあるかもしれない.
あとはリファレンスさえしっかり作ってくれれば2016年以降流行る可能性があるかもしれない.
むしろ流行ってくれ.