プログラミング言語Lean 4の現状 - 檜山正幸のキマイラ飼育記 (はてなBlog)証明支援系Lean〈リーン〉は、かなり前（2017年くらい）から注目しているソフトウェアです。注目はしているんですが、ちゃんと調べる機会がなかったので、このブログで触れたことはありませんでした。2022年のうちに紹介したい（今は大晦日の夜）。 Leanは現在、バージョン3系とバージョン4系が混在しています。このため情報が錯綜していて、分かりにくい状況になっています。今はバージョン3系が使われていますが、これからLeanを使い始めるならバージョン4をインストールしてもいいかも知れません（ただし、開発バージョンであることは承知の上で）。 Leanは、CoqやIsabelleと同様、証明支援系〈proof assistant〉として設計開発されました。実際、機械可読な定理記述のために広く使われています。 バージョン4になりLeanは、汎用プログラミング言語としての機能・特性を前面に打ち出してきま
