License	Windows	Linux / macOS	Test Coverage	Chat

About

• Homepage
• Theorem Proving in Lean
• Core library
• Change Log
• FAQ
• For HoTT mode, please use Lean2.

Installation

Stable and nightly binary releases of Lean are available on the homepage. For building Lean from source, see the build instructions.

Miscellaneous

• Building Doxygen Documentation: doxygen src/Doxyfile
• Coding Style
• Library Style Conventions
• Git Commit Conventions
• Automatic Builds
• Syntax Highlight Lean Code in LaTeX
• Exporting, and reference type-checkers

Roadmap

• Open RFC issues
• Features
• Wish list
• High priority issues
• Medium priority issues