Useful Lean resources

A collection of useful resources to help you master Lean

  • The official site is the main repository for content about the language. It has an online playground where you can try out the language without installing anything.
  • The Reservoir indexes, builds and tests packages within the Lean and Lake ecosystem. It is the place to go for third-party packages.
  • Lean Community is a collaborative, open-source network around the Lean ecosystem. It is responsible for mathlib, the main community-driven mathematics library for Lean 4.
  • Lean 4 Zulip Chat is the main chat for the Lean Community.