Documentation

The current version of Lean is Lean 3, and is under active development. The source code and libraries can be found on github.

Using Lean

Tutorials

Each of the following tutorials is available in an online version that runs alongside a Lean in your browser, and as a PDF document.

  • An Introduction to Lean
    A quick tour of Lean and its features.
    online tutorial, pdf

  • Theorem Proving in Lean
    A introduction to using Lean as an interactive theorem prover.
    online tutorial, pdf

  • Programming in Lean
    An introduction to writing and reasoning about programs in Lean, as well as writing tactics and automation.
    online tutorial, pdf

Caveat: all three are incomplete and under construction.

Lean 2

The previous version of Lean is still being maintained but not developed. Lean 2 has special support for homotopy type theory and a substantial library. The source code and libraries can be found on github.

Forum

You are welcome to join the Lean user forum on Google Groups.