Skip to main content

Lean 3 is the previous version of the Lean theorem prover, and has an active "community" release. If using the final "official" release from 2019 (3.4.2) which is incompatible with [mathlib], make this clear in your question.

While the final official Lean 3 release of 3.4.2 was in 2019, the community continues to actively release newer versions in order to support mathlib development. Typically, "Lean 3" refers to this community version.

Lean 3.4.2 (GitHub)
Note: See install instructions instead of installing directly from GitHub.

Lean Community (Site)
Chat (Zulip)
Lean Community (GitHub)

Theorem Proving in Lean
The Natural Number Game

Code Language (used for syntax highlighting): lang-hs