Documentation

Functional Programming in Lean

The standard introduction to using Lean as a programming language.

Theorem Proving in Lean 4

The standard introduction to using Lean as a theorem prover.

The Lean Language Reference

A detailed description of the syntax, semantics, and standard library of Lean. Use this to look up specifics.

More Resources

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 learning resources page of the community website lists many further tutorials and documentation sources for Lean 4.

Setting Up Lean

Most users only need to install the VS Code extension, which takes care of everything else. More details are available in the setup guide. It's important to ensure that your editor is set up to show semantic tokens.

Tour

The tour provides a brief introduction to Lean, showing how to define functions and types.

Examples

Palindromes: Inductively-defined predicates are used to specify palindromes. This specification is used to prove the correctness of a function that checks whether a list is, in fact, a palindrome.
Binary Search Trees: A verified implementation of binary search trees.
A Certified Type Checker: A specification of a simple type system together with a type checker that's proven correct.
The Well-Typed Interpreter: Dependent types are used to rule out run-time errors for a small interpreter.
Dependent de Bruijn Indices: In a simply-typed lambda-calculus, variables are encoded as intrinsically-typed references into a context, capturing both the number of intervening binders and the corresponding type. This representation is then used as the basis for a constant folding pass, which is proved correct.
Parametric Higher-Order Abstract Syntax (PHOAS): Intrinsically-typed terms are represented in the PHOAS style, which is a higher-order encoding that's suitable for interactive theorem provers based on full dependent types. This is used to implement constant folding and prove it correct.
Metaprogramming: Balanced Parentheses: A demonstration of Lean's syntax extension capabilities in which new syntax rules are added that match parentheses and braces.
Metaprogramming: Arithmetic Expressions: A more involved example of syntax extension that demonstrates the use of precedence and associativity.

Online Discussions