Leanの学び方

Leanは、関数型の汎用プログラミング言語であると同時に、証明支援システムでもあります。Leanを学ぶためのリソースは数多くあり、プログラミング言語としての側面に焦点を当てたものもあれば、定理証明器としての使い方に焦点を当てたものもあります。

Functional Programming in Leanは、Leanを使って関数型プログラミングのパラダイムを紹介する入門書です。関数型プログラミング言語の経験がまったくなくても、Leanを学びたいというプログラマーを対象としています。

Leanでの定理証明をより深く学びたい場合には、Theorem Proving in Lean 4が公式リソースとして挙げられています。

The Lean Language Referenceは、言語の詳細な情報についての最も信頼できる情報源です。

Leanの学習に役立つリソースは、ほかにもLean Communityが多数公開しています。