The Lean Reference

Updated 7 months ago


This document is the primary reference for the Lean programming language.

It focuses on providing:

  • Informal explanations of the language and its use.
  • A formal presentation of Lean's meta theory and axioms.
  • A description of the languages runtime, async proof checking ...

This document is not intended to be an introduction to the language. We provide separate books intended to for most users of Lean, one focused on theorem proving and another on programming with Lean.

This document only covers the minimal library details needed by Lean, the standard library is documented separately, with the hope of using leandoc to extract and host documentation elsewhere in the future.