Skip to content

Commit

Permalink
docs: update best-of list for version 2024.11.07
Browse files Browse the repository at this point in the history
  • Loading branch information
34j authored and actions-user committed Nov 7, 2024
1 parent 1375521 commit c7f29c5
Show file tree
Hide file tree
Showing 4 changed files with 100 additions and 33 deletions.
64 changes: 32 additions & 32 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@
</p>

<!-- prettier-ignore -->
This curated list contains 45 awesome open-source projects with a total of 10K 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!
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](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).
Expand Down Expand Up @@ -61,14 +61,14 @@ _Quick reference with short text_

<details><summary><b><a href="https://leanprover-community.github.io/mathlib-overview.html">A mathlib overview</a></b> (🥇15 · ⭐ 53) - Hosts the website for mathlib and other Lean community.. <code><a href="http://bit.ly/34MBwT8">MIT</a></code></summary>

- [GitHub](https://github.com/leanprover-community/leanprover-community.github.io) (👨‍💻 120 · 🔀 120 · 📋 37 - 59% open · ⏱️ 28.10.2024):
- [GitHub](https://github.com/leanprover-community/leanprover-community.github.io) (👨‍💻 120 · 🔀 120 · 📋 37 - 59% open · ⏱️ 04.11.2024):

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

</details>
<details><summary><b><a href="https://github.com/madvorak/lean4-tactics">Lean 4 Tactics</a></b> (🥈7 · ⭐ 56) - Overview of tactics in Lean 4 for beginners longer version. <code><a href="http://bit.ly/3rvuUlR">Unlicense</a></code></summary>
<details><summary><b><a href="https://github.com/madvorak/lean4-tactics">Lean 4 Tactics</a></b> (🥈6 · ⭐ 57 · 📉) - Overview of tactics in Lean 4 for beginners longer version. <code><a href="http://bit.ly/3rvuUlR">Unlicense</a></code></summary>

- [GitHub](https://github.com/madvorak/lean4-tactics) (👨‍💻 2 · 🔀 2 · ⏱️ 19.09.2024):

Expand Down Expand Up @@ -131,9 +131,9 @@ _Quick reference with short text_

_Tutorials with long text_

<details><summary><b><a href="https://github.com/leanprover-community/lean4-metaprogramming-book">A Lean 4 Metaprogramming Book</a></b> (🥇16 · ⭐ 220) - Practical manual with code that goes into the.. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code></summary>
<details><summary><b><a href="https://github.com/leanprover-community/lean4-metaprogramming-book">A Lean 4 Metaprogramming Book</a></b> (🥇15 · ⭐ 220 · 📉) - Practical manual with code that goes into the.. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code></summary>

- [GitHub](https://github.com/leanprover-community/lean4-metaprogramming-book) (👨‍💻 23 · 🔀 54 · 📥 100 · 📋 39 - 43% open · ⏱️ 07.10.2024):
- [GitHub](https://github.com/leanprover-community/lean4-metaprogramming-book) (👨‍💻 24 · 🔀 54 · 📥 12 · 📋 39 - 43% open · ⏱️ 05.11.2024):

```
git clone https://github.com/leanprover-community/lean4-metaprogramming-book
Expand All @@ -142,7 +142,7 @@ _Tutorials with long text_
</details>
<details><summary><b><a href="https://lean-lang.org/theorem_proving_in_lean4/">Theorem Proving in Lean 4</a></b> (🥈12 · ⭐ 160) - Theorem Proving in Lean 4. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code></summary>

- [GitHub](https://github.com/leanprover/theorem_proving_in_lean4) (👨‍💻 80 · 🔀 88 · 📋 37 - 64% open · ⏱️ 14.10.2024):
- [GitHub](https://github.com/leanprover/theorem_proving_in_lean4) (👨‍💻 80 · 🔀 88 · 📋 39 - 66% open · ⏱️ 14.10.2024):

```
git clone https://github.com/leanprover/theorem_proving_in_lean4
Expand All @@ -158,18 +158,18 @@ _Tutorials with long text_
```

</details>
<details><summary><b><a href="https://hrmacbeth.github.io/math2001/">The mechanics of proof</a></b> (🥉10 · ⭐ 200) - Early university level course. <code>❗Unlicensed</code></summary>
<details><summary><b><a href="https://hrmacbeth.github.io/math2001/">The mechanics of proof</a></b> (🥈11 · ⭐ 200 · 📈) - Early university level course. <code>❗Unlicensed</code></summary>

- [GitHub](https://github.com/hrmacbeth/math2001) (🔀 75 · 📋 16 - 56% open · ⏱️ 18.10.2024):
- [GitHub](https://github.com/hrmacbeth/math2001) (🔀 77 · 📋 16 - 56% open · ⏱️ 01.11.2024):

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

</details>
<details><summary><b><a href="https://lean-lang.org/functional_programming_in_lean/">Functional Programming in Lean</a></b> (🥉7 · ⭐ 70 · 💤) - Functional Programming in Lean. <code>❗Unlicensed</code></summary>
<details><summary><b><a href="https://lean-lang.org/functional_programming_in_lean/">Functional Programming in Lean</a></b> (🥉7 · ⭐ 71 · 💤) - Functional Programming in Lean. <code>❗Unlicensed</code></summary>

- [GitHub](https://github.com/leanprover/fp-lean) (👨‍💻 2 · 🔀 20 · 📥 73 · 📋 150 - 32% open · ⏱️ 06.02.2024):
- [GitHub](https://github.com/leanprover/fp-lean) (👨‍💻 2 · 🔀 20 · 📥 73 · 📋 150 - 33% open · ⏱️ 06.02.2024):

```
git clone https://github.com/leanprover/fp-lean
Expand All @@ -190,9 +190,9 @@ _Tutorials with long text_

_Actual Lean 4 code for learning purposes_

<details><summary><b><a href="https://github.com/yuma-mizuno/lean-math-workshop">Lean Math Workshop</a></b> (🥇10 · ⭐ 68 · 📈) - Materials for a workshop held in Japan. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code> <code>ja</code></summary>
<details><summary><b><a href="https://github.com/yuma-mizuno/lean-math-workshop">Lean Math Workshop</a></b> (🥇10 · ⭐ 69) - Materials for a workshop held in Japan. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code> <code>ja</code></summary>

- [GitHub](https://github.com/yuma-mizuno/lean-math-workshop) (👨‍💻 5 · 🔀 21 · 📋 13 - 7% open · ⏱️ 13.07.2024):
- [GitHub](https://github.com/yuma-mizuno/lean-math-workshop) (👨‍💻 5 · 🔀 22 · 📋 13 - 7% open · ⏱️ 13.07.2024):

```
git clone https://github.com/yuma-mizuno/lean-math-workshop
Expand All @@ -201,7 +201,7 @@ _Actual Lean 4 code for learning purposes_
</details>
<details><summary><b><a href="https://github.com/eric-wieser/lean-matrix-cookbook">The Matrix Cookbook, using Lean's mathlib</a></b> (🥉7 · ⭐ 84) - The matrix cookbook, proved in the Lean theorem prover. <code><a href="http://bit.ly/34MBwT8">MIT</a></code></summary>

- [GitHub](https://github.com/eric-wieser/lean-matrix-cookbook) (👨‍💻 2 · 🔀 10 · ⏱️ 02.10.2024):
- [GitHub](https://github.com/eric-wieser/lean-matrix-cookbook) (👨‍💻 2 · 🔀 11 · ⏱️ 02.10.2024):

```
git clone https://github.com/eric-wieser/lean-matrix-cookbook
Expand All @@ -218,7 +218,7 @@ _Reusable Lean 4 code for enhancing usability_

<details><summary><b><a href="https://github.com/leanprover-community/ProofWidgets4">ProofWidgets</a></b> (🥇19 · ⭐ 110) - Helper toolkit for creating your own Lean 4 UserWidgets. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code></summary>

- [GitHub](https://github.com/leanprover-community/ProofWidgets4) (👨‍💻 14 · 🔀 26 · 📥 360K · 📋 20 - 65% open · ⏱️ 20.10.2024):
- [GitHub](https://github.com/leanprover-community/ProofWidgets4) (👨‍💻 14 · 🔀 26 · 📥 360K · 📋 20 - 65% open · ⏱️ 04.11.2024):

```
git clone https://github.com/leanprover-community/ProofWidgets4
Expand All @@ -244,16 +244,16 @@ _Reusable Lean 4 code (theorems, etc.)_

<details><summary><b><a href="https://github.com/lecopivo/SciLean">SciLean</a></b> (🥇15 · ⭐ 320) - Scientific computing in Lean 4. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code></summary>

- [GitHub](https://github.com/lecopivo/SciLean) (👨‍💻 9 · 🔀 29 · 📋 33 - 54% open · ⏱️ 23.10.2024):
- [GitHub](https://github.com/lecopivo/SciLean) (👨‍💻 9 · 🔀 29 · 📋 34 - 55% open · ⏱️ 07.11.2024):

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

</details>
<details><summary><b><a href="https://github.com/leanprover-community/aesop">aesop</a></b> (🥇15 · ⭐ 200) - Proof search tactic (Automated Extensible Search for Obvious Proofs). <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code></summary>
<details><summary><b><a href="https://github.com/leanprover-community/aesop">aesop</a></b> (🥇15 · ⭐ 210) - Proof search tactic (Automated Extensible Search for Obvious Proofs). <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code></summary>

- [GitHub](https://github.com/leanprover-community/aesop) (👨‍💻 20 · 🔀 27 · 📋 63 - 34% open · ⏱️ 22.10.2024):
- [GitHub](https://github.com/leanprover-community/aesop) (👨‍💻 20 · 🔀 28 · 📋 63 - 34% open · ⏱️ 06.11.2024):

```
git clone https://github.com/leanprover-community/aesop
Expand All @@ -262,14 +262,14 @@ _Reusable Lean 4 code (theorems, etc.)_
</details>
<details><summary><b><a href="https://github.com/ufmg-smite/lean-smt">SMT Lean</a></b> (🥈10 · ⭐ 100) - Tactics for discharging Lean goals into SMT solvers. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code></summary>

- [GitHub](https://github.com/ufmg-smite/lean-smt) (👨‍💻 8 · 🔀 20 · 📋 16 - 43% open · ⏱️ 26.10.2024):
- [GitHub](https://github.com/ufmg-smite/lean-smt) (👨‍💻 8 · 🔀 20 · 📋 17 - 47% open · ⏱️ 26.10.2024):

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

</details>
<details><summary><b><a href="https://github.com/verified-optimization/CvxLean">CvxLean</a></b> (🥈10 · ⭐ 39) - Convex optimization modeling in Lean 4. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code></summary>
<details><summary><b><a href="https://github.com/verified-optimization/CvxLean">CvxLean</a></b> (🥈10 · ⭐ 40) - Convex optimization modeling in Lean 4. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code></summary>

- [GitHub](https://github.com/verified-optimization/CvxLean) (👨‍💻 3 · 🔀 4 · ⏱️ 20.05.2024):

Expand Down Expand Up @@ -306,7 +306,7 @@ _Core Lean 4 code_

<details><summary><b><a href="https://github.com/leanprover/lean4">lean4</a></b> (🥇32 · ⭐ 4.7K) - Lean 4 repository. Includes `Lake`. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code></summary>

- [GitHub](https://github.com/leanprover/lean4) (👨‍💻 200 · 🔀 420 · 📥 430K · 📋 1.9K - 30% open · ⏱️ 31.10.2024):
- [GitHub](https://github.com/leanprover/lean4) (👨‍💻 200 · 🔀 420 · 📥 450K · 📋 1.9K - 30% open · ⏱️ 07.11.2024):

```
git clone https://github.com/leanprover/lean4
Expand All @@ -315,25 +315,25 @@ _Core Lean 4 code_
</details>
<details><summary><b><a href="https://github.com/leanprover-community/mathlib4">mathlib4</a></b> (🥈25 · ⭐ 1.5K) - Math library. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code></summary>

- [GitHub](https://github.com/leanprover-community/mathlib4) (👨‍💻 350 · 🔀 320 · 📋 410 - 55% open · ⏱️ 31.10.2024):
- [GitHub](https://github.com/leanprover-community/mathlib4) (👨‍💻 360 · 🔀 330 · 📋 410 - 55% open · ⏱️ 07.11.2024):

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

</details>
<details><summary><b><a href="https://github.com/leanprover/elan">elan</a></b> (🥈19 · ⭐ 320) - Version Manager. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code></summary>
<details><summary><b><a href="https://github.com/leanprover/elan">elan</a></b> (🥈20 · ⭐ 320 · 📈) - Version Manager. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code></summary>

- [GitHub](https://github.com/leanprover/elan) (👨‍💻 20 · 🔀 35 · 📥 810K · 📋 75 - 32% open · ⏱️ 08.10.2024):
- [GitHub](https://github.com/leanprover/elan) (👨‍💻 21 · 🔀 35 · 📥 830K · 📋 75 - 32% open · ⏱️ 06.11.2024):

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

</details>
<details><summary><b><a href="https://github.com/leanprover-community/batteries">std4</a></b> (🥉16 · ⭐ 240) - Standard Library. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code></summary>
<details><summary><b><a href="https://github.com/leanprover-community/batteries">std4</a></b> (🥉16 · ⭐ 250) - Standard Library. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code></summary>

- [GitHub](https://github.com/leanprover-community/batteries) (👨‍💻 62 · 🔀 100 · 📋 61 - 37% open · ⏱️ 31.10.2024):
- [GitHub](https://github.com/leanprover-community/batteries) (👨‍💻 62 · 🔀 100 · 📋 61 - 37% open · ⏱️ 05.11.2024):

```
git clone https://github.com/leanprover/std4
Expand All @@ -342,16 +342,16 @@ _Core Lean 4 code_
</details>
<details><summary><b><a href="https://github.com/leanprover/doc-gen4">doc-gen4</a></b> (🥉14 · ⭐ 65) - Document Generator. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code></summary>

- [GitHub](https://github.com/leanprover/doc-gen4) (👨‍💻 31 · 🔀 41 · 📋 81 - 33% open · ⏱️ 16.10.2024):
- [GitHub](https://github.com/leanprover/doc-gen4) (👨‍💻 31 · 🔀 41 · 📋 82 - 34% open · ⏱️ 04.11.2024):

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

</details>
<details><summary><b><a href="https://github.com/leanprover-community/quote4">quote4</a></b> (🥉10 · ⭐ 74) - Intuitive, type-safe expression quotations for Lean 4. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code></summary>
<details><summary><b><a href="https://github.com/leanprover-community/quote4">quote4</a></b> (🥉10 · ⭐ 75) - Intuitive, type-safe expression quotations for Lean 4. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code></summary>

- [GitHub](https://github.com/leanprover-community/quote4) (👨‍💻 8 · 🔀 12 · 📋 22 - 59% open · ⏱️ 18.10.2024):
- [GitHub](https://github.com/leanprover-community/quote4) (👨‍💻 8 · 🔀 12 · 📋 22 - 59% open · ⏱️ 04.11.2024):

```
git clone https://github.com/leanprover-community/quote4
Expand Down Expand Up @@ -399,16 +399,16 @@ _Tools not made in Lean 4_

<details><summary><b><a href="https://github.com/leanprover/vscode-lean4">vscode-lean4</a></b> (🥇20 · ⭐ 170) - Visual Studio Code extension. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code></summary>

- [GitHub](https://github.com/leanprover/vscode-lean4) (👨‍💻 58 · 🔀 48 · 📥 440 · 📋 210 - 21% open · ⏱️ 29.10.2024):
- [GitHub](https://github.com/leanprover/vscode-lean4) (👨‍💻 58 · 🔀 48 · 📥 440 · 📋 210 - 21% open · ⏱️ 06.11.2024):

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

</details>
<details><summary><b><a href="https://github.com/lean-dojo/LeanDojo">LeanDojo</a></b> (🥈17 · ⭐ 560) - Tool for data extraction and interacting with Lean programmatically. <code><a href="http://bit.ly/34MBwT8">MIT</a></code></summary>
<details><summary><b><a href="https://github.com/lean-dojo/LeanDojo">LeanDojo</a></b> (🥈17 · ⭐ 570) - Tool for data extraction and interacting with Lean programmatically. <code><a href="http://bit.ly/34MBwT8">MIT</a></code></summary>

- [GitHub](https://github.com/lean-dojo/LeanDojo) (👨‍💻 17 · 🔀 88 · 📋 63 - 6% open · ⏱️ 13.10.2024):
- [GitHub](https://github.com/lean-dojo/LeanDojo) (👨‍💻 17 · 🔀 89 · 📋 64 - 7% open · ⏱️ 13.10.2024):

```
git clone https://github.com/lean-dojo/LeanDojo
Expand All @@ -417,7 +417,7 @@ _Tools not made in Lean 4_
</details>
<details><summary><b><a href="https://github.com/Paper-Proof/paperproof">Paperproof</a></b> (🥈17 · ⭐ 360) - Theorem proving interface which feels like pen-and-paper proofs. <code><a href="http://bit.ly/34MBwT8">MIT</a></code></summary>

- [GitHub](https://github.com/Paper-Proof/paperproof) (👨‍💻 5 · 🔀 9 · 📋 34 - 32% open · ⏱️ 15.10.2024):
- [GitHub](https://github.com/Paper-Proof/paperproof) (👨‍💻 5 · 🔀 9 · 📋 34 - 32% open · ⏱️ 04.11.2024):

```
git clone https://github.com/Paper-Proof/paperproof
Expand Down
13 changes: 13 additions & 0 deletions history/2024-11-07_changes.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
## 📈 Trending Up

_Projects that have a higher project-quality score compared to the last update. There might be a variety of reasons, such as increased downloads or code activity._

- <b><a href="https://github.com/leanprover/elan">elan</a></b> (🥈20 · ⭐ 320 · 📈) - Version Manager. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code>
- <b><a href="https://hrmacbeth.github.io/math2001/">The mechanics of proof</a></b> (🥈11 · ⭐ 200 · 📈) - Early university level course. <code>❗Unlicensed</code>

## 📉 Trending Down

_Projects that have a lower project-quality score compared to the last update. There might be a variety of reasons such as decreased downloads or code activity._

- <b><a href="https://github.com/leanprover-community/lean4-metaprogramming-book">A Lean 4 Metaprogramming Book</a></b> (🥇15 · ⭐ 220 · 📉) - Practical manual with code that goes into the.. <code><a href="http://bit.ly/3nYMfla">Apache-2</a></code>
- <b><a href="https://github.com/madvorak/lean4-tactics">Lean 4 Tactics</a></b> (🥈6 · ⭐ 57 · 📉) - Overview of tactics in Lean 4 for beginners longer version. <code><a href="http://bit.ly/3rvuUlR">Unlicense</a></code>
Loading

0 comments on commit c7f29c5

Please sign in to comment.