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