best-of-lean4

🏆  A ranked list of awesome projects. Updated weekly.

This curated list contains 46 awesome open-source projects with a total of 16K stars grouped into 11 categories. All projects are ranked by a project-quality score, which is calculated based on various metrics automatically collected from GitHub and different package managers. If you like to add or update projects, feel free to ~open an [issue](https://github.com/34j/best-of-lean4/issues/new/choose)~, submit a [pull request](https://github.com/34j/best-of-lean4/pulls), or **_directly edit the [projects.yaml](https://github.com/34j/best-of-lean4/edit/main/projects.yaml)_**. Contributions are very welcome! > 🧙‍♂️ Discover other [best-of lists](https://best-of.org) or [create your own](https://github.com/best-of-lists/best-of/blob/main/create-best-of-list.md). ## Contents - [Cheatsheets](#cheatsheets) _9 projects_ - [Tutorials](#tutorials) _7 projects_ - [Samples](#samples) _2 projects_ - [Packages (Meta)](#packages-meta) _2 projects_ - [Packages](#packages) _6 projects_ - [Core packages](#core-packages) _6 projects_ - [Games](#games) _1 projects_ - [Community](#community) _2 projects_ - [Tools](#tools) _6 projects_ - [Other awesome lists](#other-awesome-lists) _3 projects_ - [Movies](#movies) _2 projects_ ## Explanation - 🥇🥈🥉  Combined project-quality score - ⭐️  Star count from GitHub - 🐣  New project _(less than 6 months old)_ - 💤  Inactive project _(6 months no activity)_ - 💀  Dead project _(12 months no activity)_ - 📈📉  Project is trending up or down - ➕  Project was recently added - ❗️  Warning _(e.g. missing/risky license)_ - 👨‍💻  Contributors count from GitHub - 🔀  Fork count from GitHub - 📋  Issue count from GitHub - ⏱️  Last update timestamp on package manager - 📥  Download count from package manager - 📦  Number of dependent projects
## Cheatsheets Back to top _Quick reference with short text_
A mathlib overview (🥇17 · ⭐ 64) - Hosts the website for mathlib and other Lean community.. MIT - [GitHub](https://github.com/leanprover-community/leanprover-community.github.io) (👨‍💻 150 · 🔀 160 · 📋 42 - 42% open · ⏱️ 25.09.2025): ``` git clone https://github.com/leanprover-community/leanprover-community.github.io ```
Lean 4 Tactics (🥈8 · ⭐ 91) - Overview of tactics in Lean 4 for beginners longer version. Unlicense - [GitHub](https://github.com/madvorak/lean4-tactics) (👨‍💻 3 · 🔀 3 · ⏱️ 26.06.2025): ``` git clone https://github.com/madvorak/lean4-tactics ```
lean3-tactic-lean4 (🥈6 · ⭐ 27 · 💤) - Reference sheet for people who know Lean 3 and want.. Unlicense Lean 3 - [GitHub](https://github.com/madvorak/lean3-tactic-lean4) (👨‍💻 2 · 🔀 3 · ⏱️ 13.11.2024): ``` git clone https://github.com/madvorak/lean3-tactic-lean4 ```
Lean by Example (🥈6) - Lean. MIT ja - [GitHub](https://github.com/lean-ja/lean-ja.github.io) (👨‍💻 3 · ⏱️ 22.07.2025): ``` git clone https://github.com/lean-ja/lean-ja.github.io ```
Lean 4 Cheatsheet (🥉5 · ⭐ 30 · 💤) - Printable (A4) overview of tactics in Lean 4 for.. Unlicense - [GitHub](https://github.com/madvorak/lean4-cheatsheet) (🔀 1 · ⏱️ 19.09.2024): ``` git clone https://github.com/madvorak/lean4-cheatsheet ```
(Mathlib4) General Documentation (API Reference) (🥉5 · ⭐ 9) - Official Mathlib API Reference. ❗Unlicensed - [GitHub](https://github.com/leanprover-community/mathlib4_docs) (👨‍💻 7 · 🔀 5 · ⏱️ 02.09.2025): ``` git clone https://github.com/leanprover-community/mathlib4_docs ```
Moogle: Semantic search over mathlib4 (🥉1) - Better performance (latency) than `General.. ❗Unlicensed - _No project information available._
`#help` command output (🥉1) - Output of `#help option`, `#help attr`, ... shown in.. ❗Unlicensed - _No project information available._
Show 1 hidden projects... - cs-dm/CheatSheet.lean (🥈6 · ⭐ 16 · 💀) - CS2012 UVa CS Discrete Math Spring 2018. ❗Unlicensed Lean 3

## Tutorials Back to top _Tutorials with long text_
A Lean 4 Metaprogramming Book (🥇14 · ⭐ 260 · 💤) - Practical manual with code that goes into the.. Apache-2 - [GitHub](https://github.com/leanprover-community/lean4-metaprogramming-book) (👨‍💻 26 · 🔀 65 · 📥 810 · 📋 44 - 45% open · ⏱️ 28.02.2025): ``` git clone https://github.com/leanprover-community/lean4-metaprogramming-book ```
Theorem Proving in Lean 4 (🥈13 · ⭐ 210) - Theorem Proving in Lean 4. Apache-2 - [GitHub](https://github.com/leanprover/theorem_proving_in_lean4) (👨‍💻 81 · 🔀 99 · 📋 59 - 76% open · ⏱️ 10.09.2025): ``` git clone https://github.com/leanprover/theorem_proving_in_lean4 ```
Mathematics in Lean (🥈12 · ⭐ 410 · 📈) - Note that there are many parts of the documentation.. Apache-2 - [GitHub](https://github.com/leanprover-community/mathematics_in_lean) (👨‍💻 3 · 🔀 280 · ⏱️ 08.08.2025): ``` git clone https://github.com/leanprover-community/mathematics_in_lean ```
Functional Programming in Lean (🥉11 · ⭐ 110 · 📈) - Functional Programming in Lean. ❗Unlicensed - [GitHub](https://github.com/leanprover/fp-lean) (👨‍💻 4 · 🔀 47 · 📥 110 · 📋 180 - 24% open · ⏱️ 10.09.2025): ``` git clone https://github.com/leanprover/fp-lean ```
The mechanics of proof (🥉9 · ⭐ 300 · 💤) - Early university level course. ❗Unlicensed - [GitHub](https://github.com/hrmacbeth/math2001) (🔀 140 · 📋 23 - 65% open · ⏱️ 09.12.2024): ``` git clone https://github.com/hrmacbeth/math2001 ```
The Lean Reference Manual (🥉1) - Official Lean 3 Reference Manual. ❗Unlicensed Lean 3 - _No project information available._
Lean Manual (🥉1) - Official Manual. ❗Unlicensed - _No project information available._

## Samples Back to top _Actual Lean 4 code for learning purposes_
Lean Math Workshop (🥇12 · ⭐ 86) - Materials for a workshop held in Japan. Apache-2 ja - [GitHub](https://github.com/yuma-mizuno/lean-math-workshop) (👨‍💻 5 · 🔀 25 · 📋 14 - 14% open · ⏱️ 05.09.2025): ``` git clone https://github.com/yuma-mizuno/lean-math-workshop ```
The Matrix Cookbook, using Lean's mathlib (🥉9 · ⭐ 120 · 📈) - The matrix cookbook, proved in the Lean theorem prover. MIT - [GitHub](https://github.com/eric-wieser/lean-matrix-cookbook) (👨‍💻 3 · 🔀 17 · 📋 3 - 33% open · ⏱️ 16.09.2025): ``` git clone https://github.com/eric-wieser/lean-matrix-cookbook ```

## Packages (Meta) Back to top _Reusable Lean 4 code for enhancing usability_
ProofWidgets (🥇20 · ⭐ 160) - Helper toolkit for creating your own Lean 4 UserWidgets. Apache-2 - [GitHub](https://github.com/leanprover-community/ProofWidgets4) (👨‍💻 20 · 🔀 39 · 📥 900K · 📋 28 - 42% open · ⏱️ 18.09.2025): ``` git clone https://github.com/leanprover-community/ProofWidgets4 ```
Show 1 hidden projects... - llmstep (🥉8 · ⭐ 140 · 💀) - llmstep: [L]LM proofstep suggestions in Lean 4. MIT

## Packages Back to top _Reusable Lean 4 code (theorems, etc.)_
aesop (🥇15 · ⭐ 300) - Proof search tactic (Automated Extensible Search for Obvious Proofs). Apache-2 - [GitHub](https://github.com/leanprover-community/aesop) (👨‍💻 26 · 🔀 36 · 📋 85 - 43% open · ⏱️ 15.09.2025): ``` git clone https://github.com/leanprover-community/aesop ```
SciLean (🥈14 · ⭐ 430) - Scientific computing in Lean 4. Apache-2 - [GitHub](https://github.com/lecopivo/SciLean) (👨‍💻 10 · 🔀 36 · 📋 47 - 55% open · ⏱️ 09.06.2025): ``` git clone https://github.com/lecopivo/SciLean ```
SMT Lean (🥈13 · ⭐ 220 · 📈) - Tactics for discharging Lean goals into SMT solvers. Apache-2 - [GitHub](https://github.com/ufmg-smite/lean-smt) (👨‍💻 10 · 🔀 28 · 📋 26 - 42% open · ⏱️ 18.09.2025): ``` git clone https://github.com/ufmg-smite/lean-smt ```
lean-crypto (🥉8 · ⭐ 44 · 💤) - Cryptographic routines for the Lean 4 language. Apache-2 - [GitHub](https://github.com/joehendrix/lean-crypto) (👨‍💻 3 · 🔀 3 · ⏱️ 09.09.2024): ``` git clone https://github.com/joehendrix/lean-crypto ```
Show 2 hidden projects... - CvxLean (🥉10 · ⭐ 54 · 💀) - Convex optimization modeling in Lean 4. Apache-2 - SATurn (🥉6 · ⭐ 60 · 💀) - Experiments with SAT solvers with proofs in Lean 4. MIT

## Core packages Back to top _Core Lean 4 code_
lean4 (🥇33 · ⭐ 6.5K) - Lean 4 repository. Includes `Lake`. Apache-2 - [GitHub](https://github.com/leanprover/lean4) (👨‍💻 250 · 🔀 660 · 📥 1.6M · 📋 2.6K - 28% open · ⏱️ 25.09.2025): ``` git clone https://github.com/leanprover/lean4 ```
mathlib4 (🥈25 · ⭐ 2.4K) - Math library. Apache-2 - [GitHub](https://github.com/leanprover-community/mathlib4) (👨‍💻 550 · 🔀 780 · 📋 530 - 51% open · ⏱️ 25.09.2025): ``` git clone https://github.com/leanprover-community/mathlib4 ```
elan (🥈21 · ⭐ 430) - Version Manager. Apache-2 - [GitHub](https://github.com/leanprover/elan) (👨‍💻 28 · 🔀 47 · 📥 1.6M · 📋 93 - 35% open · ⏱️ 22.09.2025): ``` git clone https://github.com/leanprover/elan ```
std4 (🥉20 · ⭐ 330) - Standard Library. Apache-2 - [GitHub](https://github.com/leanprover-community/batteries) (👨‍💻 78 · 🔀 130 · 📥 62 · 📋 71 - 35% open · ⏱️ 23.09.2025): ``` git clone https://github.com/leanprover/std4 ```
doc-gen4 (🥉14 · ⭐ 100) - Document Generator. Apache-2 - [GitHub](https://github.com/leanprover/doc-gen4) (👨‍💻 42 · 🔀 52 · 📋 91 - 24% open · ⏱️ 16.09.2025): ``` git clone https://github.com/leanprover/doc-gen4 ```
quote4 (🥉11 · ⭐ 97) - Intuitive, type-safe expression quotations for Lean 4. Apache-2 - [GitHub](https://github.com/leanprover-community/quote4) (👨‍💻 12 · 🔀 16 · 📋 28 - 67% open · ⏱️ 23.09.2025): ``` git clone https://github.com/leanprover-community/quote4 ```

## Games Back to top _Lean 4 Games_
Lean Game Server (🥇17 · ⭐ 320 · 📉) - Mainly for Natural Number Game. Be careful not to.. ❗️GPL-3.0 - [GitHub](https://github.com/leanprover-community/lean4game) (👨‍💻 32 · 🔀 57 · 📋 280 - 33% open · ⏱️ 24.09.2025): ``` git clone https://github.com/leanprover-community/lean4game ```

## Community Back to top _Community_
Zulip chat for discussions about Lean and mathlib (🥇1) - Official community. ❗Unlicensed - _No project information available._
Lean 4 Anarchy (Discord) (🥇1) - Anarchy discord server. ❗Unlicensed - _No project information available._

## Tools Back to top _Tools not made in Lean 4_
LeanCopilot (🥇20 · ⭐ 1.2K) - LLMs as Copilots for Theorem Proving in Lean. MIT - [GitHub](https://github.com/lean-dojo/LeanCopilot) (👨‍💻 14 · 🔀 110 · 📥 4.2K · 📋 60 - 3% open · ⏱️ 15.09.2025): ``` git clone https://github.com/lean-dojo/LeanCopilot ```
vscode-lean4 (🥇20 · ⭐ 230) - Visual Studio Code extension. Apache-2 - [GitHub](https://github.com/leanprover/vscode-lean4) (👨‍💻 69 · 🔀 76 · 📥 630 · 📋 240 - 22% open · ⏱️ 25.09.2025): ``` git clone https://github.com/leanprover/vscode-lean4 ```
LeanDojo (🥈16 · ⭐ 710) - Tool for data extraction and interacting with Lean programmatically. MIT - [GitHub](https://github.com/lean-dojo/LeanDojo) (👨‍💻 21 · 🔀 110 · 📋 85 - 5% open · ⏱️ 13.09.2025): ``` git clone https://github.com/lean-dojo/LeanDojo ```
Paperproof (🥈16 · ⭐ 460) - Theorem proving interface which feels like pen-and-paper proofs. MIT - [GitHub](https://github.com/Paper-Proof/paperproof) (👨‍💻 5 · 🔀 12 · 📋 39 - 33% open · ⏱️ 22.07.2025): ``` git clone https://github.com/Paper-Proof/paperproof ```
lean4web (🥉11 · ⭐ 110 · 📉) - Web editor. Apache-2 - [GitHub](https://github.com/leanprover-community/lean4web) (👨‍💻 13 · 🔀 38 · 📋 53 - 15% open · ⏱️ 07.09.2025): ``` git clone https://github.com/leanprover-community/lean4web ```
Reservoir (🥉11 · ⭐ 24 · 📈) - Lakes package registry. Apache-2 - [GitHub](https://github.com/leanprover/reservoir) (👨‍💻 4 · 🔀 6 · 📋 36 - 36% open · ⏱️ 09.09.2025): ``` git clone https://github.com/leanprover/reservoir ```

## Other awesome lists Back to top
LEAN JA リンク集 (🥇6) - Japanese translated versions of several tutorials are available. (). MIT ja - [GitHub](https://github.com/lean-ja/lean-ja.github.io) (👨‍💻 3 · ⏱️ 22.07.2025): ``` git clone https://github.com/lean-ja/lean-ja.github.io ```
Links (lean-lang.org) (🥉1) - Official collection of links. ❗Unlicensed - _No project information available._
lean4 - Where is the syntax of Lean 4 documented? - Proof Assistants Stack Exchange (🥉1) - Discussion regarding Lean 4 documentation. ❗Unlicensed - _No project information available._

## Movies Back to top
lean4 - YouTube (🥇1) - YouTube movies. ❗Unlicensed - _No project information available._
人気の「Lean」動画 14本 - ニコニコ動画 (🥇1) - Niconico movies. Entertaining instructions using TTS.. ❗Unlicensed ja - _No project information available._
--- ## Related Resources - [**Best-of lists**](https://best-of.org): Discover other best-of lists with awesome open-source projects on all kinds of topics. ## Contribution Contributions are encouraged and always welcome! If you like to add or update projects, choose one of the following ways: - Open an issue by selecting one of the provided categories from the [issue page](https://github.com/34j/best-of-lean4/issues/new/choose) and fill in the requested information. - Modify the [projects.yaml](https://github.com/34j/best-of-lean4/blob/main/projects.yaml) with your additions or changes, and submit a pull request. This can also be done directly via the [Github UI](https://github.com/34j/best-of-lean4/edit/main/projects.yaml). If you like to contribute to or share suggestions regarding the project metadata collection or markdown generation, please refer to the [best-of-generator](https://github.com/best-of-lists/best-of-generator) repository. If you like to create your own best-of list, we recommend to follow [this guide](https://github.com/best-of-lists/best-of/blob/main/create-best-of-list.md). For more information on how to add or update projects, please read the [contribution guidelines](https://github.com/34j/best-of-lean4/blob/main/CONTRIBUTING.md). By participating in this project, you agree to abide by its [Code of Conduct](https://github.com/34j/best-of-lean4/blob/main/.github/CODE_OF_CONDUCT.md). ## License [![CC0](https://mirrors.creativecommons.org/presskit/buttons/88x31/svg/by-sa.svg)](https://creativecommons.org/licenses/by-sa/4.0/)