如何學習 Lean

從零開始學習 Lean 的入門概觀

Lean 既是一種函式式的通用程式語言，也是一套證明輔助工具。學習 Lean 的資源相當多，有些著重於它的程式設計面，有些則著重於將它當作定理證明器使用。

Functional Programming in Lean 這本書以 Lean 介紹函式式程式設計範式。它的對象是想學 Lean 的程式設計者，即使他們先前完全沒有接觸過函式式程式語言的經驗。

若想更深入認識 Lean 中的定理證明，Theorem Proving in Lean 4 這本書被列為官方資源。

The Lean Language Reference 是取得該語言詳細資訊的權威來源。

Lean Community 提供了許多其他學習 Lean 的資源。