How to learn Lean

Lean is both a functional general-purpose programming language and a proof assistant. There are numerous resources available for learning Lean, some focusing on its programming aspects and others on its use as a theorem prover.

The book Functional Programming in Lean is an introduction to the functional programming paradigm using Lean. It is aimed at programmers who want to learn Lean, even if they have no prior experience with functional programming languages.

For a more in-depth look at theorem proving in Lean, the book Theorem Proving in Lean 4 is listed as an official resource.

The Lean Language Reference is the authoritative source for detailed information about the language.

Many additional resources for learning Lean are made available by the Lean Community.