如何学习 Lean

从零开始上手 Lean 的入门概览

Lean 既是一门函数式通用编程语言，也是一个证明助手。 学习 Lean 的资源有很多，有些侧重它的编程方面，有些侧重它作为定理证明器的用途。

Functional Programming in Lean 是一本用 Lean 讲解函数式编程范式的入门书。 它面向想学习 Lean 的程序员，即使此前完全没有函数式编程语言的经验也能读懂。

如果想更深入地了解 Lean 中的定理证明，Theorem Proving in Lean 4 这本书被列为官方资源。

The Lean Language Reference 是了解这门语言详细信息的权威来源。

Lean Community 还提供了许多其他学习 Lean 的资源。