This is a snapshot of the Lean 0.2 theorem prover. We have this separate repository because this version has special support for Homotopy Type Theory.

About

• Latest version
• Homepage
• Theorem Proving in Lean: HTML, PDF
• Standard Library
• HoTT Library
• Emacs Mode

Requirements

• C++11 compatible compiler: g++ (version >= 4.8.1), or clang++ (version >= 3.3)
• CMake
• GMP (GNU multiprecision library)
• MPFR (GNU MPFR Library)
• Lua 5.2 or 5.1, or LuaJIT 2.0

Installing

Windows

• MSys2

Linux

• Ubuntu 12.04 or newer (detailed)
• Ubuntu 12.04 or newer (brief)
• Fedora 19

OS X

• OS X 10.9

Build Instructions

• CMake + Make
• CMake + Ninja
• Faster builds with ccache

Miscellaneous

• Building Doxygen Documentation: doxygen src/Doxyfile
• Coding Style
• Library Style Conventions
• Git Commit Conventions
• Syntax Highlight Lean Code in LaTeX