best-of-lean4

🏆  A ranked list of awesome projects. Updated weekly.

This curated list contains 45 awesome open-source projects with a total of 11K 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, submit a pull request, or directly edit the projects.yaml. Contributions are very welcome!

🧙‍♂️ Discover other best-of lists or create your own.

Contents

• Cheatsheets 9 projects
• Tutorials 7 projects
• Samples 2 projects
• Packages (Meta) 2 projects
• Packages 6 projects
• Core packages 6 projects
• Games 1 projects
• Community 2 projects
• Tools 5 projects
• Other awesome lists 3 projects
• 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

Quick reference with short text

A mathlib overview (🥇15 · ⭐ 55) - Hosts the website for mathlib and other Lean community.. MIT

• GitHub (👨‍💻 120 · 🔀 120 · 📋 38 - 57% open · ⏱️ 26.11.2024):

  ```
  git clone https://github.com/leanprover-community/leanprover-community.github.io
  ```
  

lean3-tactic-lean4 (🥈6 · ⭐ 25 · 📈) - Reference sheet for people who know Lean 3 and want.. Unlicense Lean 3

GitHub (👨‍💻 2 · 🔀 2 · ⏱️ 13.11.2024):

```
git clone https://github.com/madvorak/lean3-tactic-lean4
```

Lean by Example (🥈6) - Lean. MIT ja

GitHub (👨‍💻 3 · ⏱️ 18.06.2024):

```
git clone https://github.com/lean-ja/lean-ja.github.io
```

Lean 4 Tactics (🥉5 · ⭐ 61) - Overview of tactics in Lean 4 for beginners longer version. Unlicense

GitHub (👨‍💻 2 · 🔀 2 · ⏱️ 19.09.2024):

```
git clone https://github.com/madvorak/lean4-tactics
```

Lean 4 Cheatsheet (🥉4 · ⭐ 23) - Printable (A4) overview of tactics in Lean 4 for beginners. Unlicense

GitHub (🔀 1 · ⏱️ 19.09.2024):

```
git clone https://github.com/madvorak/lean4-cheatsheet
```

(Mathlib4) General Documentation (API Reference) (🥉4 · ⭐ 8) - Official Mathlib API Reference. ❗Unlicensed

GitHub (👨‍💻 5 · 🔀 2 · ⏱️ 09.12.2024):

```
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 · ⭐ 15 · 💀) - CS2012 UVa CS Discrete Math Spring 2018. ❗Unlicensed Lean 3

Tutorials

Tutorials with long text

A Lean 4 Metaprogramming Book (🥇15 · ⭐ 230) - Practical manual with code that goes into the.. Apache-2

• GitHub (👨‍💻 24 · 🔀 55 · 📥 110 · 📋 39 - 43% open · ⏱️ 05.11.2024):

  ```
  git clone https://github.com/leanprover-community/lean4-metaprogramming-book
  ```
  

Theorem Proving in Lean 4 (🥈12 · ⭐ 170) - Theorem Proving in Lean 4. Apache-2

GitHub (👨‍💻 80 · 🔀 90 · 📋 42 - 69% open · ⏱️ 14.10.2024):

```
git clone https://github.com/leanprover/theorem_proving_in_lean4
```

The mechanics of proof (🥈11 · ⭐ 210) - Early university level course. ❗Unlicensed

GitHub (🔀 80 · 📋 17 - 52% open · ⏱️ 09.12.2024):

```
git clone https://github.com/hrmacbeth/math2001
```

Mathematics in Lean (🥉10 · ⭐ 280 · 📉) - Note that there are many parts of the documentation.. ❗Unlicensed

GitHub (👨‍💻 3 · 🔀 190 · ⏱️ 02.12.2024):

```
git clone https://github.com/leanprover-community/mathematics_in_lean
```

Functional Programming in Lean (🥉8 · ⭐ 73 · 💤) - Functional Programming in Lean. ❗Unlicensed

GitHub (👨‍💻 2 · 🔀 21 · 📥 74 · 📋 160 - 35% open · ⏱️ 06.02.2024):

```
git clone https://github.com/leanprover/fp-lean
```

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

Actual Lean 4 code for learning purposes

Lean Math Workshop (🥇10 · ⭐ 73) - Materials for a workshop held in Japan. Apache-2 ja

• GitHub (👨‍💻 5 · 🔀 22 · 📋 14 - 14% open · ⏱️ 13.07.2024):

  ```
  git clone https://github.com/yuma-mizuno/lean-math-workshop
  ```
  

The Matrix Cookbook, using Lean's mathlib (🥉7 · ⭐ 88) - The matrix cookbook, proved in the Lean theorem prover. MIT

GitHub (👨‍💻 2 · 🔀 11 · ⏱️ 23.11.2024):

```
git clone https://github.com/eric-wieser/lean-matrix-cookbook
```

Packages (Meta)

Reusable Lean 4 code for enhancing usability

ProofWidgets (🥇19 · ⭐ 120) - Helper toolkit for creating your own Lean 4 UserWidgets. Apache-2

• GitHub (👨‍💻 14 · 🔀 26 · 📥 390K · 📋 21 - 57% open · ⏱️ 12.12.2024):

  ```
  git clone https://github.com/leanprover-community/ProofWidgets4
  ```
  

Show 1 hidden projects...

llmstep (🥉8 · ⭐ 120 · 💀) - llmstep: [L]LM proofstep suggestions in Lean 4. MIT

Packages

Reusable Lean 4 code (theorems, etc.)

SciLean (🥇15 · ⭐ 340) - Scientific computing in Lean 4. Apache-2

• GitHub (👨‍💻 9 · 🔀 30 · 📋 39 - 56% open · ⏱️ 09.12.2024):

  ```
  git clone https://github.com/lecopivo/SciLean
  ```
  

aesop (🥈14 · ⭐ 220 · 📉) - Proof search tactic (Automated Extensible Search for Obvious Proofs). Apache-2

GitHub (👨‍💻 20 · 🔀 27 · 📋 64 - 34% open · ⏱️ 05.12.2024):

```
git clone https://github.com/leanprover-community/aesop
```

SMT Lean (🥈10 · ⭐ 150) - Tactics for discharging Lean goals into SMT solvers. Apache-2

GitHub (👨‍💻 8 · 🔀 19 · 📋 17 - 47% open · ⏱️ 05.12.2024):

```
git clone https://github.com/ufmg-smite/lean-smt
```

CvxLean (🥈10 · ⭐ 42 · 💤) - Convex optimization modeling in Lean 4. Apache-2

GitHub (👨‍💻 3 · 🔀 4 · ⏱️ 20.05.2024):

```
git clone https://github.com/verified-optimization/CvxLean
```

lean-crypto (🥉8 · ⭐ 41) - Cryptographic routines for the Lean 4 language. Apache-2

GitHub (👨‍💻 3 · 🔀 3 · ⏱️ 09.09.2024):

```
git clone https://github.com/joehendrix/lean-crypto
```

SATurn (🥉6 · ⭐ 53) - Experiments with SAT solvers with proofs in Lean 4. MIT

GitHub (👨‍💻 2 · 🔀 2 · ⏱️ 23.06.2024):

```
git clone https://github.com/siddhartha-gadgil/Saturn
```

Core packages

Core Lean 4 code

lean4 (🥇32 · ⭐ 4.8K) - Lean 4 repository. Includes `Lake`. Apache-2

• GitHub (👨‍💻 210 · 🔀 430 · 📥 520K · 📋 2K - 30% open · ⏱️ 12.12.2024):

  ```
  git clone https://github.com/leanprover/lean4
  ```
  

mathlib4 (🥈25 · ⭐ 1.6K) - Math library. Apache-2

GitHub (👨‍💻 370 · 🔀 340 · 📋 420 - 55% open · ⏱️ 12.12.2024):

```
git clone https://github.com/leanprover-community/mathlib4
```

elan (🥈21 · ⭐ 320 · 📈) - Version Manager. Apache-2

GitHub (👨‍💻 22 · 🔀 36 · 📥 900K · 📋 77 - 33% open · ⏱️ 11.12.2024):

```
git clone https://github.com/leanprover/elan
```

std4 (🥉18 · ⭐ 260 · 📈) - Standard Library. Apache-2

GitHub (👨‍💻 66 · 🔀 110 · 📥 1 · 📋 62 - 32% open · ⏱️ 12.12.2024):

```
git clone https://github.com/leanprover/std4
```

doc-gen4 (🥉14 · ⭐ 68) - Document Generator. Apache-2

GitHub (👨‍💻 33 · 🔀 43 · 📋 85 - 29% open · ⏱️ 12.12.2024):

```
git clone https://github.com/leanprover/doc-gen4
```

quote4 (🥉10 · ⭐ 75) - Intuitive, type-safe expression quotations for Lean 4. Apache-2

GitHub (👨‍💻 8 · 🔀 12 · 📋 22 - 59% open · ⏱️ 02.12.2024):

```
git clone https://github.com/leanprover-community/quote4
```

Games

Lean 4 Games

Lean Game Server (🥇17 · ⭐ 200 · 📈) - Mainly for Natural Number Game. Be careful not to.. ❗️GPL-3.0

• GitHub (👨‍💻 21 · 🔀 34 · 📋 230 - 32% open · ⏱️ 10.12.2024):

  ```
  git clone https://github.com/leanprover-community/lean4game
  ```
  

Community

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

Tools not made in Lean 4

vscode-lean4 (🥇20 · ⭐ 170) - Visual Studio Code extension. Apache-2

• GitHub (👨‍💻 58 · 🔀 50 · 📥 460 · 📋 210 - 20% open · ⏱️ 10.12.2024):

  ```
  git clone https://github.com/leanprover/vscode-lean4
  ```
  

LeanDojo (🥈16 · ⭐ 590 · 📉) - Tool for data extraction and interacting with Lean programmatically. MIT

GitHub (👨‍💻 17 · 🔀 94 · 📋 66 - 6% open · ⏱️ 08.12.2024):

```
git clone https://github.com/lean-dojo/LeanDojo
```

Paperproof (🥈16 · ⭐ 370 · 📉) - Theorem proving interface which feels like pen-and-paper proofs. MIT

GitHub (👨‍💻 5 · 🔀 10 · 📋 34 - 32% open · ⏱️ 13.11.2024):

```
git clone https://github.com/Paper-Proof/paperproof
```

lean4web (🥉11 · ⭐ 71 · 📉) - Web editor. Apache-2

GitHub (👨‍💻 7 · 🔀 20 · 📋 37 - 21% open · ⏱️ 24.11.2024):

```
git clone https://github.com/leanprover-community/lean4web
```

Reservoir (🥉8 · ⭐ 17) - Lakes package registry. Apache-2

GitHub (🔀 1 · 📋 25 - 24% open · ⏱️ 19.10.2024):

```
git clone https://github.com/leanprover/reservoir
```

Other awesome lists

LEAN JA リンク集 (🥇6) - Japanese translated versions of several tutorials are available. (). MIT ja

• GitHub (👨‍💻 3 · ⏱️ 18.06.2024):

  ```
  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

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: 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 and fill in the requested information.
• Modify the projects.yaml with your additions or changes, and submit a pull request. This can also be done directly via the Github UI.

If you like to contribute to or share suggestions regarding the project metadata collection or markdown generation, please refer to the best-of-generator repository. If you like to create your own best-of list, we recommend to follow this guide.

For more information on how to add or update projects, please read the contribution guidelines. By participating in this project, you agree to abide by its Code of Conduct.

License