Documentation

• Functional Programming in Lean is the standard reference for learning how to use Lean as a programming language.

• Theorem Proving in Lean 4 is the standard reference for learning how to use Lean as a theorem prover.

• Mathematics in Lean is an alternative resource for learning how to use Lean for formalizing mathematics specifically.

• The Mechanics of Proof is a set of lecture notes dealing with how to write careful, rigorous mathematical proofs. These lecture notes are aimed at the early university level and have been written for the course Math 2001, at Fordham University.

• The Lean Language Reference describes the syntax, semantics, and standard library of Lean.

• The Documentation Overview contains examples, a developer's guide, and other documentation.

The learning resources page of the community website lists many further tutorials and documentation sources for Lean 4.

Chat Room

A public chat room dedicated to Lean is open on Zulip.