Skip to content
Lean Theorem Prover
C++ Lean CMake C Shell Python Other
Branch: master
Clone or download
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
.github fix(docs): Update github issue hyperlinks (#75) Nov 9, 2019
bin fix(bin/leanpkg): handle spaces in paths on POSIX systems Oct 27, 2018
doc feat(tactic): make docstrings of imported modules accessible (#81) Nov 22, 2019
extras/latex chore(extras/depgraph): remove leandeps Jul 15, 2017
images chore(CMakeLists.txt): move Lean logo to make sure we can test leanem… Feb 1, 2015
leanpkg feat(io): better file existence api (#31) Apr 27, 2019
library
packages chore(script/test_registry): Replace with leanpkg. Execute in every a… Dec 20, 2017
script chore(build): disable tracing May 14, 2019
src fix(library/check): do not assign metavariables in tactic.type_check (#… Dec 3, 2019
tests fix(library/check): do not assign metavariables in tactic.type_check (#… Dec 3, 2019
tmp chore(tmp/lean4.md): moved to google docs Mar 21, 2018
.appveyor.yml chore(.appveyor.yml): fix non-nightly builds Apr 16, 2018
.clang-format
.codecov.yml fix(.codecov.yml): do not fail github ci if coverage drops by 0.01% Jun 25, 2017
.gitattributes chore(.gitattributes): use `union` merge strategy for doc/changes.md Dec 11, 2017
.gitignore feat(tactic/add_def_eqns): add a Lean function to access the equation… May 7, 2019
.travis.yml fix(build): fix emscripten build in travis (#68) Oct 1, 2019
LICENSE Add LICENSE file Jul 16, 2013
README.md fix(docs): Update github issue hyperlinks (#75) Nov 9, 2019

README.md

logo

LicenseWindowsLinux / macOSTest CoverageChat
Codecov Join the Zulip chat

About

  • Homepage
  • Theorem Proving in Lean
  • Change Log
  • FAQ
  • Important: Lean 3.4.2 is the latest release. It is also the last release for the Lean 3.x code base. Only major bugs (e.g., soundness) will be fixed for this code base from now on. We are currently developing Lean 4 in a new (private) repository. The Lean 4 source code will be released here when ready. The main goals for Lean 4 are described here.
  • 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

Roadmap

You can’t perform that action at this time.