TehMillhouse/lean

Lean Theorem Prover

License	Windows	Linux / macOS	Test Coverage	Chat

About

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

Requirements

• C++11 compatible compiler
• CMake
• GMP (GNU multiprecision library)

Build Instructions

• Linux (Ubuntu)
• Windows (msys2)
• macOS

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