From 15da3185fe32c9f336d22bc56056b290c0a3ceb2 Mon Sep 17 00:00:00 2001
From: 34j <34j@users.noreply.github.com>
Date: Thu, 19 Dec 2024 09:09:01 +0000
Subject: [PATCH] docs: update best-of list for version 2024.12.19
---
README.md | 88 ++++++++++++++++-----------------
history/2024-12-19_changes.md | 16 ++++++
history/2024-12-19_projects.csv | 46 +++++++++++++++++
latest-changes.md | 17 +++----
4 files changed, 113 insertions(+), 54 deletions(-)
create mode 100644 history/2024-12-19_changes.md
create mode 100644 history/2024-12-19_projects.csv
diff --git a/README.md b/README.md
index 747b7c0..c4aedb4 100644
--- a/README.md
+++ b/README.md
@@ -61,41 +61,41 @@ _Quick reference with short text_
A mathlib overview (🥇15 · ⭐ 55) - Hosts the website for mathlib and other Lean community.. MIT
-- [GitHub](https://github.com/leanprover-community/leanprover-community.github.io) (👨💻 120 · 🔀 120 · 📋 38 - 57% open · ⏱️ 26.11.2024):
+- [GitHub](https://github.com/leanprover-community/leanprover-community.github.io) (👨💻 120 · 🔀 120 · 📋 38 - 57% open · ⏱️ 18.12.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
+ Lean 4 Tactics (🥈6 · ⭐ 63 · 📈) - Overview of tactics in Lean 4 for beginners longer version. Unlicense
-- [GitHub](https://github.com/madvorak/lean3-tactic-lean4) (👨💻 2 · 🔀 2 · ⏱️ 13.11.2024):
+- [GitHub](https://github.com/madvorak/lean4-tactics) (👨💻 2 · 🔀 2 · ⏱️ 19.09.2024):
```
- git clone https://github.com/madvorak/lean3-tactic-lean4
+ git clone https://github.com/madvorak/lean4-tactics
```
Lean by Example (🥈6) - Lean. MIT ja
+ lean3-tactic-lean4 (🥈6 · ⭐ 25) - Reference sheet for people who know Lean 3 and want.. Unlicense Lean 3
-- [GitHub](https://github.com/lean-ja/lean-ja.github.io) (👨💻 3 · ⏱️ 18.06.2024):
+- [GitHub](https://github.com/madvorak/lean3-tactic-lean4) (👨💻 2 · 🔀 2 · ⏱️ 13.11.2024):
```
- git clone https://github.com/lean-ja/lean-ja.github.io
+ git clone https://github.com/madvorak/lean3-tactic-lean4
```
Lean 4 Tactics (🥉5 · ⭐ 61) - Overview of tactics in Lean 4 for beginners longer version. Unlicense
+ Lean by Example (🥈6) - Lean. MIT ja
-- [GitHub](https://github.com/madvorak/lean4-tactics) (👨💻 2 · 🔀 2 · ⏱️ 19.09.2024):
+- [GitHub](https://github.com/lean-ja/lean-ja.github.io) (👨💻 3 · ⏱️ 18.06.2024):
```
- git clone https://github.com/madvorak/lean4-tactics
+ git clone https://github.com/lean-ja/lean-ja.github.io
```
Lean 4 Cheatsheet (🥉4 · ⭐ 23) - Printable (A4) overview of tactics in Lean 4 for beginners. Unlicense
+ Lean 4 Cheatsheet (🥉5 · ⭐ 23 · 📈) - Printable (A4) overview of tactics in Lean 4 for.. Unlicense
- [GitHub](https://github.com/madvorak/lean4-cheatsheet) (🔀 1 · ⏱️ 19.09.2024):
@@ -104,9 +104,9 @@ _Quick reference with short text_
```
(Mathlib4) General Documentation (API Reference) (🥉4 · ⭐ 8) - Official Mathlib API Reference. ❗Unlicensed
+ (Mathlib4) General Documentation (API Reference) (🥉5 · ⭐ 8 · 📈) - Official Mathlib API Reference. ❗Unlicensed
-- [GitHub](https://github.com/leanprover-community/mathlib4_docs) (👨💻 5 · 🔀 2 · ⏱️ 09.12.2024):
+- [GitHub](https://github.com/leanprover-community/mathlib4_docs) (👨💻 6 · 🔀 3 · ⏱️ 18.12.2024):
```
git clone https://github.com/leanprover-community/mathlib4_docs
@@ -133,7 +133,7 @@ _Tutorials with long text_
A Lean 4 Metaprogramming Book (🥇15 · ⭐ 230) - Practical manual with code that goes into the.. Apache-2
-- [GitHub](https://github.com/leanprover-community/lean4-metaprogramming-book) (👨💻 24 · 🔀 55 · 📥 110 · 📋 39 - 43% open · ⏱️ 05.11.2024):
+- [GitHub](https://github.com/leanprover-community/lean4-metaprogramming-book) (👨💻 24 · 🔀 55 · 📥 140 · 📋 39 - 43% open · ⏱️ 05.11.2024):
```
git clone https://github.com/leanprover-community/lean4-metaprogramming-book
@@ -142,28 +142,28 @@ _Tutorials with long text_
Theorem Proving in Lean 4 (🥈12 · ⭐ 170) - Theorem Proving in Lean 4. Apache-2
-- [GitHub](https://github.com/leanprover/theorem_proving_in_lean4) (👨💻 80 · 🔀 90 · 📋 42 - 69% open · ⏱️ 14.10.2024):
+- [GitHub](https://github.com/leanprover/theorem_proving_in_lean4) (👨💻 80 · 🔀 91 · 📋 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
+ Mathematics in Lean (🥈10 · ⭐ 290) - Note that there are many parts of the documentation.. ❗Unlicensed
-- [GitHub](https://github.com/hrmacbeth/math2001) (🔀 80 · 📋 17 - 52% open · ⏱️ 09.12.2024):
+- [GitHub](https://github.com/leanprover-community/mathematics_in_lean) (👨💻 3 · 🔀 190 · ⏱️ 02.12.2024):
```
- git clone https://github.com/hrmacbeth/math2001
+ git clone https://github.com/leanprover-community/mathematics_in_lean
```
Mathematics in Lean (🥉10 · ⭐ 280 · 📉) - Note that there are many parts of the documentation.. ❗Unlicensed
+ The mechanics of proof (🥈10 · ⭐ 210 · 📉) - Early university level course. ❗Unlicensed
-- [GitHub](https://github.com/leanprover-community/mathematics_in_lean) (👨💻 3 · 🔀 190 · ⏱️ 02.12.2024):
+- [GitHub](https://github.com/hrmacbeth/math2001) (🔀 81 · 📋 17 - 52% open · ⏱️ 09.12.2024):
```
- git clone https://github.com/leanprover-community/mathematics_in_lean
+ git clone https://github.com/hrmacbeth/math2001
```
The Matrix Cookbook, using Lean's mathlib (🥉7 · ⭐ 88) - The matrix cookbook, proved in the Lean theorem prover. MIT
+ The Matrix Cookbook, using Lean's mathlib (🥉7 · ⭐ 90) - The matrix cookbook, proved in the Lean theorem prover. MIT
- [GitHub](https://github.com/eric-wieser/lean-matrix-cookbook) (👨💻 2 · 🔀 11 · ⏱️ 23.11.2024):
@@ -218,7 +218,7 @@ _Reusable Lean 4 code for enhancing usability_
ProofWidgets (🥇19 · ⭐ 120) - Helper toolkit for creating your own Lean 4 UserWidgets. Apache-2
-- [GitHub](https://github.com/leanprover-community/ProofWidgets4) (👨💻 14 · 🔀 26 · 📥 390K · 📋 21 - 57% open · ⏱️ 12.12.2024):
+- [GitHub](https://github.com/leanprover-community/ProofWidgets4) (👨💻 14 · 🔀 27 · 📥 400K · 📋 23 - 60% open · ⏱️ 12.12.2024):
```
git clone https://github.com/leanprover-community/ProofWidgets4
@@ -237,16 +237,16 @@ _Reusable Lean 4 code for enhancing usability_
_Reusable Lean 4 code (theorems, etc.)_
-SciLean (🥇15 · ⭐ 340) - Scientific computing in Lean 4. Apache-2
+SciLean (🥇15 · ⭐ 350) - Scientific computing in Lean 4. Apache-2
-- [GitHub](https://github.com/lecopivo/SciLean) (👨💻 9 · 🔀 30 · 📋 39 - 56% open · ⏱️ 09.12.2024):
+- [GitHub](https://github.com/lecopivo/SciLean) (👨💻 9 · 🔀 30 · 📋 39 - 56% open · ⏱️ 17.12.2024):
```
git clone https://github.com/lecopivo/SciLean
```
aesop (🥈14 · ⭐ 220 · 📉) - Proof search tactic (Automated Extensible Search for Obvious Proofs). Apache-2
+ aesop (🥈14 · ⭐ 220) - Proof search tactic (Automated Extensible Search for Obvious Proofs). Apache-2
- [GitHub](https://github.com/leanprover-community/aesop) (👨💻 20 · 🔀 27 · 📋 64 - 34% open · ⏱️ 05.12.2024):
@@ -257,7 +257,7 @@ _Reusable Lean 4 code (theorems, etc.)_
SMT Lean (🥈10 · ⭐ 150) - Tactics for discharging Lean goals into SMT solvers. Apache-2
-- [GitHub](https://github.com/ufmg-smite/lean-smt) (👨💻 8 · 🔀 19 · 📋 17 - 47% open · ⏱️ 05.12.2024):
+- [GitHub](https://github.com/ufmg-smite/lean-smt) (👨💻 8 · 🔀 19 · 📋 17 - 47% open · ⏱️ 17.12.2024):
```
git clone https://github.com/ufmg-smite/lean-smt
@@ -273,7 +273,7 @@ _Reusable Lean 4 code (theorems, etc.)_
```
lean-crypto (🥉8 · ⭐ 41) - Cryptographic routines for the Lean 4 language. Apache-2
+ lean-crypto (🥉8 · ⭐ 42) - Cryptographic routines for the Lean 4 language. Apache-2
- [GitHub](https://github.com/joehendrix/lean-crypto) (👨💻 3 · 🔀 3 · ⏱️ 09.09.2024):
@@ -301,7 +301,7 @@ _Core Lean 4 code_
lean4 (🥇32 · ⭐ 4.8K) - Lean 4 repository. Includes `Lake`. Apache-2
-- [GitHub](https://github.com/leanprover/lean4) (👨💻 210 · 🔀 430 · 📥 520K · 📋 2K - 30% open · ⏱️ 12.12.2024):
+- [GitHub](https://github.com/leanprover/lean4) (👨💻 210 · 🔀 430 · 📥 540K · 📋 2K - 30% open · ⏱️ 19.12.2024):
```
git clone https://github.com/leanprover/lean4
@@ -310,41 +310,41 @@ _Core Lean 4 code_
mathlib4 (🥈25 · ⭐ 1.6K) - Math library. Apache-2
-- [GitHub](https://github.com/leanprover-community/mathlib4) (👨💻 370 · 🔀 340 · 📋 420 - 55% open · ⏱️ 12.12.2024):
+- [GitHub](https://github.com/leanprover-community/mathlib4) (👨💻 370 · 🔀 340 · 📋 420 - 55% open · ⏱️ 18.12.2024):
```
git clone https://github.com/leanprover-community/mathlib4
```
elan (🥈21 · ⭐ 320 · 📈) - Version Manager. Apache-2
+ elan (🥈21 · ⭐ 330) - Version Manager. Apache-2
-- [GitHub](https://github.com/leanprover/elan) (👨💻 22 · 🔀 36 · 📥 900K · 📋 77 - 33% open · ⏱️ 11.12.2024):
+- [GitHub](https://github.com/leanprover/elan) (👨💻 22 · 🔀 36 · 📥 910K · 📋 77 - 33% open · ⏱️ 11.12.2024):
```
git clone https://github.com/leanprover/elan
```
std4 (🥉18 · ⭐ 260 · 📈) - Standard Library. Apache-2
+ std4 (🥉18 · ⭐ 260) - Standard Library. Apache-2
-- [GitHub](https://github.com/leanprover-community/batteries) (👨💻 66 · 🔀 110 · 📥 1 · 📋 62 - 32% open · ⏱️ 12.12.2024):
+- [GitHub](https://github.com/leanprover-community/batteries) (👨💻 66 · 🔀 110 · 📥 2 · 📋 62 - 32% open · ⏱️ 12.12.2024):
```
git clone https://github.com/leanprover/std4
```
doc-gen4 (🥉14 · ⭐ 68) - Document Generator. Apache-2
+ doc-gen4 (🥉15 · ⭐ 69 · 📈) - Document Generator. Apache-2
-- [GitHub](https://github.com/leanprover/doc-gen4) (👨💻 33 · 🔀 43 · 📋 85 - 29% open · ⏱️ 12.12.2024):
+- [GitHub](https://github.com/leanprover/doc-gen4) (👨💻 33 · 🔀 44 · 📋 85 - 27% open · ⏱️ 19.12.2024):
```
git clone https://github.com/leanprover/doc-gen4
```
quote4 (🥉10 · ⭐ 75) - Intuitive, type-safe expression quotations for Lean 4. Apache-2
+ quote4 (🥉10 · ⭐ 76) - Intuitive, type-safe expression quotations for Lean 4. Apache-2
- [GitHub](https://github.com/leanprover-community/quote4) (👨💻 8 · 🔀 12 · 📋 22 - 59% open · ⏱️ 02.12.2024):
@@ -361,9 +361,9 @@ _Core Lean 4 code_
_Lean 4 Games_
-Lean Game Server (🥇17 · ⭐ 200 · 📈) - Mainly for Natural Number Game. Be careful not to.. ❗️GPL-3.0
+Lean Game Server (🥇17 · ⭐ 210) - Mainly for Natural Number Game. Be careful not to.. ❗️GPL-3.0
-- [GitHub](https://github.com/leanprover-community/lean4game) (👨💻 21 · 🔀 34 · 📋 230 - 32% open · ⏱️ 10.12.2024):
+- [GitHub](https://github.com/leanprover-community/lean4game) (👨💻 21 · 🔀 35 · 📋 230 - 32% open · ⏱️ 10.12.2024):
```
git clone https://github.com/leanprover-community/lean4game
@@ -394,14 +394,14 @@ _Tools not made in Lean 4_
vscode-lean4 (🥇20 · ⭐ 170) - Visual Studio Code extension. Apache-2
-- [GitHub](https://github.com/leanprover/vscode-lean4) (👨💻 58 · 🔀 50 · 📥 460 · 📋 210 - 20% open · ⏱️ 10.12.2024):
+- [GitHub](https://github.com/leanprover/vscode-lean4) (👨💻 58 · 🔀 51 · 📥 480 · 📋 210 - 21% open · ⏱️ 18.12.2024):
```
git clone https://github.com/leanprover/vscode-lean4
```
LeanDojo (🥈16 · ⭐ 590 · 📉) - Tool for data extraction and interacting with Lean programmatically. MIT
+ LeanDojo (🥈16 · ⭐ 590) - Tool for data extraction and interacting with Lean programmatically. MIT
- [GitHub](https://github.com/lean-dojo/LeanDojo) (👨💻 17 · 🔀 94 · 📋 66 - 6% open · ⏱️ 08.12.2024):
@@ -410,7 +410,7 @@ _Tools not made in Lean 4_
```
Paperproof (🥈16 · ⭐ 370 · 📉) - Theorem proving interface which feels like pen-and-paper proofs. MIT
+ Paperproof (🥈16 · ⭐ 370) - Theorem proving interface which feels like pen-and-paper proofs. MIT
- [GitHub](https://github.com/Paper-Proof/paperproof) (👨💻 5 · 🔀 10 · 📋 34 - 32% open · ⏱️ 13.11.2024):
@@ -419,7 +419,7 @@ _Tools not made in Lean 4_
```
lean4web (🥉11 · ⭐ 71 · 📉) - Web editor. Apache-2
+ lean4web (🥉10 · ⭐ 73 · 📉) - Web editor. Apache-2
- [GitHub](https://github.com/leanprover-community/lean4web) (👨💻 7 · 🔀 20 · 📋 37 - 21% open · ⏱️ 24.11.2024):
@@ -428,7 +428,7 @@ _Tools not made in Lean 4_
```
Reservoir (🥉8 · ⭐ 17) - Lakes package registry. Apache-2
+ Reservoir (🥉7 · ⭐ 17 · 📉) - Lakes package registry. Apache-2
- [GitHub](https://github.com/leanprover/reservoir) (🔀 1 · 📋 25 - 24% open · ⏱️ 19.10.2024):
diff --git a/history/2024-12-19_changes.md b/history/2024-12-19_changes.md
new file mode 100644
index 0000000..def7e27
--- /dev/null
+++ b/history/2024-12-19_changes.md
@@ -0,0 +1,16 @@
+## 📈 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._
+
+- doc-gen4 (🥉15 · ⭐ 69 · 📈) - Document Generator. Apache-2
+- Lean 4 Tactics (🥈6 · ⭐ 63 · 📈) - Overview of tactics in Lean 4 for beginners longer version. Unlicense
+- Lean 4 Cheatsheet (🥉5 · ⭐ 23 · 📈) - Printable (A4) overview of tactics in Lean 4 for.. Unlicense
+- (Mathlib4) General Documentation (API Reference) (🥉5 · ⭐ 8 · 📈) - Official Mathlib API Reference. ❗Unlicensed
+
+## 📉 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._
+
+- The mechanics of proof (🥈10 · ⭐ 210 · 📉) - Early university level course. ❗Unlicensed
+- lean4web (🥉10 · ⭐ 73 · 📉) - Web editor. Apache-2
+- Reservoir (🥉7 · ⭐ 17 · 📉) - Lakes package registry. Apache-2
diff --git a/history/2024-12-19_projects.csv b/history/2024-12-19_projects.csv
new file mode 100644
index 0000000..dcf0d8c
--- /dev/null
+++ b/history/2024-12-19_projects.csv
@@ -0,0 +1,46 @@
+,name,github_id,category,description,github_url,homepage,license,created_at,updated_at,last_commit_pushed_at,commit_count,recent_commit_count,fork_count,watchers_count,pr_count,open_issue_count,closed_issue_count,star_count,latest_stable_release_published_at,latest_stable_release_number,github_release_downloads,monthly_downloads,release_count,contributor_count,projectrank,show,projectrank_placing,updated_github_id,trending,labels
+0,lean4,leanprover/lean4,core,Lean 4 repository. Includes `Lake`.,https://github.com/leanprover/lean4,https://github.com/leanprover/lean4,Apache-2.0,2018-04-15 02:49:20,2024-12-19 08:36:22,2024-12-19 02:52:56,34655.0,734.0,429.0,64.0,4402.0,610.0,1389.0,4822.0,2024-12-01 23:57:48,4.14.0,535170.0,11386.0,58.0,209.0,32,True,1,,,
+1,mathlib4,leanprover-community/mathlib4,core,Math library.,https://github.com/leanprover-community/mathlib4,https://github.com/leanprover-community/mathlib4,Apache-2.0,2021-05-09 07:52:01,2024-12-19 08:51:57,2024-12-18 19:47:40,16707.0,2606.0,342.0,36.0,19624.0,237.0,188.0,1620.0,,,,,,373.0,25,True,2,,,
+2,elan,leanprover/elan,core,Version Manager.,https://github.com/leanprover/elan,https://github.com/leanprover/elan,Apache-2.0,2018-04-04 11:27:24,2024-12-11 12:08:29,2024-12-11 10:52:15,339.0,22.0,36.0,16.0,73.0,26.0,51.0,326.0,2024-02-22 22:04:49,3.1.1,911300.0,11391.0,61.0,22.0,21,True,2,,,
+3,vscode-lean4,leanprover/vscode-lean4,tool,Visual Studio Code extension.,https://github.com/leanprover/vscode-lean4,https://github.com/leanprover/vscode-lean4,Apache-2.0,2020-12-31 17:26:54,2024-12-18 07:46:09,2024-12-18 07:46:09,2653.0,35.0,51.0,11.0,338.0,45.0,168.0,173.0,2024-12-05 17:08:33,0.0.186,480.0,15.0,100.0,58.0,20,True,1,,,
+4,ProofWidgets,leanprover-community/ProofWidgets4,package-meta,Helper toolkit for creating your own Lean 4 UserWidgets.,https://github.com/leanprover-community/ProofWidgets4,https://github.com/leanprover-community/ProofWidgets4,Apache-2.0,2022-11-15 09:42:25,2024-12-12 16:36:40,2024-12-12 16:36:39,345.0,37.0,27.0,8.0,74.0,14.0,9.0,119.0,2024-12-02 03:08:17,0.0.48,396711.0,17248.0,70.0,14.0,19,True,1,,,
+5,std4,leanprover/std4,core,Standard Library.,https://github.com/leanprover-community/batteries,https://github.com/leanprover-community/batteries,Apache-2.0,2022-08-28 15:23:46,2024-12-19 09:05:54,2024-12-12 13:17:51,987.0,103.0,108.0,16.0,1013.0,20.0,42.0,256.0,2024-12-02 00:18:42,4.14.0,2.0,2.0,3.0,66.0,18,True,3,leanprover-community/batteries,,
+6,Lean Game Server,leanprover-community/lean4game,game,Mainly for Natural Number Game. Be careful not to confuse this with the [Lean 3..,https://github.com/leanprover-community/lean4game,https://adam.math.hhu.de/,GPL-3.0,2022-10-17 12:56:13,2024-12-10 17:49:31,2024-12-10 17:47:10,1066.0,21.0,35.0,11.0,45.0,75.0,154.0,208.0,2024-04-10 13:24:11,4.7.0,,,10.0,21.0,17,True,1,,,
+7,LeanDojo,lean-dojo/LeanDojo,tool,Tool for data extraction and interacting with Lean programmatically.,https://github.com/lean-dojo/LeanDojo,https://github.com/lean-dojo/LeanDojo,MIT,2023-06-13 22:04:26,2024-12-08 17:07:11,2024-12-08 17:00:22,592.0,5.0,94.0,14.0,119.0,4.0,62.0,587.0,2024-12-08 17:07:11,2.2.0,,,34.0,17.0,16,True,2,,,
+8,Paperproof,Paper-Proof/paperproof,tool,Theorem proving interface which feels like pen-and-paper proofs.,https://github.com/Paper-Proof/paperproof,https://github.com/Paper-Proof/paperproof,MIT,2023-03-16 15:24:27,2024-11-13 12:27:23,2024-11-13 12:25:47,850.0,28.0,10.0,8.0,17.0,11.0,23.0,372.0,2024-11-04 14:22:09,1.6.4,,,4.0,5.0,16,True,2,,,
+9,SciLean,lecopivo/SciLean,package,Scientific computing in Lean 4.,https://github.com/lecopivo/SciLean,https://github.com/lecopivo/SciLean,Apache-2.0,2021-09-27 21:50:10,2024-12-17 05:10:27,2024-12-17 05:10:17,1858.0,128.0,30.0,20.0,12.0,22.0,17.0,346.0,,,,,,9.0,15,True,1,,,
+10,A Lean 4 Metaprogramming Book,leanprover-community/lean4-metaprogramming-book,tutorial,Practical manual with code that goes into the internal concepts of Lean 4.,https://github.com/leanprover-community/lean4-metaprogramming-book,https://github.com/leanprover-community/lean4-metaprogramming-book,Apache-2.0,2022-03-23 22:54:03,2024-11-05 23:10:00,2024-11-05 23:08:21,281.0,7.0,55.0,9.0,110.0,17.0,22.0,230.0,,,141.0,141.0,1.0,24.0,15,True,1,,,
+11,doc-gen4,leanprover/doc-gen4,core,Document Generator.,https://github.com/leanprover/doc-gen4,https://github.com/leanprover/doc-gen4,Apache-2.0,2021-11-11 01:41:27,2024-12-19 08:05:14,2024-12-19 08:05:13,567.0,43.0,44.0,12.0,166.0,23.0,62.0,69.0,,,,,,33.0,15,True,3,,1.0,
+12,A mathlib overview,leanprover-community/leanprover-community.github.io,cheatsheet,Hosts the website for mathlib and other Lean community infrastructure.,https://github.com/leanprover-community/leanprover-community.github.io,https://leanprover-community.github.io/mathlib-overview.html,MIT,2019-01-20 17:06:26,2024-12-19 04:08:13,2024-12-18 23:25:18,10256.0,34.0,123.0,12.0,521.0,22.0,16.0,55.0,,,,,,119.0,15,True,1,,,
+13,aesop,leanprover-community/aesop,package,Proof search tactic (Automated Extensible Search for Obvious Proofs).,https://github.com/leanprover-community/aesop,https://github.com/leanprover-community/aesop,Apache-2.0,2021-06-01 13:02:59,2024-12-15 08:42:57,2024-12-05 14:23:53,813.0,20.0,27.0,9.0,121.0,22.0,42.0,221.0,,,,,,20.0,14,True,2,,,
+14,Theorem Proving in Lean 4,leanprover/theorem_proving_in_lean4,tutorial,Theorem Proving in Lean 4.,https://github.com/leanprover/theorem_proving_in_lean4,https://lean-lang.org/theorem_proving_in_lean4/,Apache-2.0,2021-08-24 18:41:32,2024-10-14 11:24:51,2024-10-14 11:24:33,1085.0,1.0,91.0,11.0,101.0,29.0,13.0,166.0,,,,,,80.0,12,True,2,,,
+15,Mathematics in Lean,leanprover-community/mathematics_in_lean,tutorial,Note that there are many parts of the documentation at leanprover-community.github.io that have not been updated.,https://github.com/leanprover-community/mathematics_in_lean,https://leanprover-community.github.io/mathematics_in_lean/,,2020-04-25 01:10:56,2024-12-02 15:39:14,2024-12-02 15:39:32,81.0,6.0,192.0,14.0,19.0,,,286.0,,,,,,3.0,10,True,2,,,
+16,The mechanics of proof,hrmacbeth/math2001,tutorial,Early university level course.,https://github.com/hrmacbeth/math2001,https://hrmacbeth.github.io/math2001/,,2022-01-24 19:33:15,2024-12-09 19:21:50,2024-12-09 19:21:47,271.0,8.0,81.0,3.0,9.0,9.0,8.0,212.0,,,,,,,10,True,2,,-1.0,
+17,SMT Lean,ufmg-smite/lean-smt,package,Tactics for discharging Lean goals into SMT solvers.,https://github.com/ufmg-smite/lean-smt,https://github.com/ufmg-smite/lean-smt,Apache-2.0,2021-11-23 20:54:14,2024-12-19 01:35:45,2024-12-17 06:37:21,137.0,29.0,19.0,9.0,140.0,8.0,9.0,148.0,,,,,,8.0,10,True,2,,,
+18,quote4,leanprover-community/quote4,core,"Intuitive, type-safe expression quotations for Lean 4.",https://github.com/leanprover-community/quote4,https://github.com/leanprover-community/quote4,Apache-2.0,2021-05-08 19:00:07,2024-12-02 03:25:39,2024-12-02 03:23:30,172.0,6.0,12.0,6.0,43.0,13.0,9.0,76.0,,,,,,8.0,10,True,3,,,
+19,lean4web,leanprover-community/lean4web,tool,Web editor.,https://github.com/leanprover-community/lean4web,https://live.lean-lang.org/,Apache-2.0,2022-10-25 08:49:35,2024-11-24 10:21:57,2024-11-24 10:21:57,344.0,2.0,20.0,10.0,9.0,8.0,29.0,73.0,,,,,,7.0,10,True,3,,-1.0,
+20,Lean Math Workshop,yuma-mizuno/lean-math-workshop,sample,Materials for a workshop held in Japan.,https://github.com/yuma-mizuno/lean-math-workshop,https://github.com/yuma-mizuno/lean-math-workshop,Apache-2.0,2023-05-30 10:58:24,2024-07-13 20:09:41,2024-07-13 20:09:40,210.0,,22.0,7.0,28.0,2.0,12.0,73.0,,,,,,5.0,10,True,1,,,['ja']
+21,CvxLean,verified-optimization/CvxLean,package,Convex optimization modeling in Lean 4.,https://github.com/verified-optimization/CvxLean,https://github.com/verified-optimization/CvxLean,Apache-2.0,2022-10-14 10:05:55,2024-05-31 12:43:00,2024-05-20 15:01:43,1237.0,,4.0,3.0,33.0,9.0,,42.0,2024-03-22 16:22:23,2.0,,,1.0,3.0,10,True,2,,,
+22,llmstep,wellecks/llmstep,package-meta,llmstep: [L]LM proofstep suggestions in Lean 4.,https://github.com/wellecks/llmstep,https://github.com/wellecks/llmstep,MIT,2023-07-08 23:50:23,2023-11-11 01:30:11,2023-11-11 01:30:11,73.0,,15.0,5.0,18.0,3.0,2.0,121.0,2023-10-31 03:18:38,1.0.0,,,1.0,5.0,8,False,3,,,
+23,Functional Programming in Lean,leanprover/fp-lean,tutorial,Functional Programming in Lean.,https://github.com/leanprover/fp-lean,https://lean-lang.org/functional_programming_in_lean/,,2022-04-07 15:40:31,2024-05-08 17:07:55,2024-02-06 09:43:13,351.0,,21.0,5.0,18.0,57.0,103.0,73.0,2022-11-27 19:58:21,pre-2022-11,74.0,2.0,5.0,2.0,8,True,3,,,
+24,lean-crypto,joehendrix/lean-crypto,package,Cryptographic routines for the Lean 4 language.,https://github.com/joehendrix/lean-crypto,https://github.com/joehendrix/lean-crypto,Apache-2.0,2021-12-13 15:25:44,2024-09-09 09:43:04,2024-09-09 09:41:06,109.0,,3.0,6.0,14.0,1.0,,42.0,,,,,,3.0,8,True,3,,,
+25,"The Matrix Cookbook, using Lean's mathlib",eric-wieser/lean-matrix-cookbook,sample,"The matrix cookbook, proved in the Lean theorem prover.",https://github.com/eric-wieser/lean-matrix-cookbook,https://github.com/eric-wieser/lean-matrix-cookbook,MIT,2021-10-21 16:25:24,2024-11-23 02:16:58,2024-11-23 02:16:58,133.0,8.0,11.0,5.0,14.0,,2.0,90.0,,,,,,2.0,7,True,3,,,
+26,Reservoir,leanprover/reservoir,tool,Lakes package registry.,https://github.com/leanprover/reservoir,https://reservoir.lean-lang.org/,Apache-2.0,2023-09-01 03:31:28,2024-10-19 06:48:56,2024-10-19 06:48:51,143.0,8.0,1.0,3.0,31.0,6.0,19.0,17.0,,,,,,,7,True,3,,-1.0,
+27,Lean 4 Tactics,madvorak/lean4-tactics,cheatsheet,Overview of tactics in Lean 4 for beginners longer version.,https://github.com/madvorak/lean4-tactics,https://github.com/madvorak/lean4-tactics,Unlicense,2023-10-04 08:11:28,2024-09-19 18:25:10,2024-09-19 18:25:09,36.0,,2.0,4.0,1.0,,,63.0,,,,,,2.0,6,True,2,,1.0,
+28,SATurn,siddhartha-gadgil/Saturn,package,Experiments with SAT solvers with proofs in Lean 4.,https://github.com/siddhartha-gadgil/Saturn,https://github.com/siddhartha-gadgil/Saturn,MIT,2021-06-03 01:41:57,2024-06-23 11:44:11,2024-06-23 11:44:08,266.0,,2.0,3.0,3.0,,1.0,53.0,,,,,,2.0,6,True,3,,,
+29,lean3-tactic-lean4,madvorak/lean3-tactic-lean4,cheatsheet,Reference sheet for people who know Lean 3 and want to write tactic-based proofs in Lean 4.,https://github.com/madvorak/lean3-tactic-lean4,https://github.com/madvorak/lean3-tactic-lean4,Unlicense,2023-02-17 15:17:58,2024-11-13 12:53:08,2024-11-13 12:53:07,51.0,5.0,2.0,1.0,1.0,,,25.0,,,,,,2.0,6,True,2,,,['lean3']
+30,cs-dm/CheatSheet.lean,kevinsullivan/cs-dm,cheatsheet,CS2012 UVa CS Discrete Math Spring 2018.,https://github.com/kevinsullivan/cs-dm,https://github.com/kevinsullivan/cs-dm/blob/master/CheatSheet.lean,,2018-01-20 02:33:29,2019-10-02 22:26:40,2019-10-02 22:26:27,480.0,,20.0,12.0,1.0,9.0,16.0,15.0,,,,,,3.0,6,False,2,,,['lean3']
+31,Lean by Example,lean-ja/lean-ja.github.io,cheatsheet,Lean.,https://github.com/lean-ja/lean-ja.github.io,https://lean-ja.github.io/lean-by-example/,MIT,2023-09-04 11:57:55,2024-06-18 10:42:09,2024-06-18 10:42:08,79.0,,,3.0,11.0,,19.0,,,,,,,3.0,6,True,2,,,['ja']
+32,LEAN JA リンク集,lean-ja/lean-ja.github.io,awesome,Japanese translated versions of several tutorials are available. ().,https://github.com/lean-ja/lean-ja.github.io,https://lean-ja.github.io/links/,MIT,2023-09-04 11:57:55,2024-06-18 10:42:09,2024-06-18 10:42:08,79.0,,,3.0,11.0,,19.0,,,,,,,3.0,6,True,1,,,['ja']
+33,Lean 4 Cheatsheet,madvorak/lean4-cheatsheet,cheatsheet,Printable (A4) overview of tactics in Lean 4 for beginners.,https://github.com/madvorak/lean4-cheatsheet,https://github.com/madvorak/lean4-cheatsheet/blob/main/lean-tactics.pdf,Unlicense,2023-03-07 15:37:12,2024-09-19 18:23:04,2024-09-19 18:22:59,12.0,,1.0,1.0,,,,23.0,,,,,,,5,True,3,,1.0,
+34,(Mathlib4) General Documentation (API Reference),leanprover-community/mathlib4_docs,cheatsheet,Official Mathlib API Reference.,https://github.com/leanprover-community/mathlib4_docs,https://leanprover-community.github.io/mathlib4_docs/,,2022-01-06 19:13:21,2024-12-18 14:34:58,2024-12-18 14:34:57,25.0,6.0,3.0,19.0,4.0,,1.0,8.0,,,,,,6.0,5,True,3,,1.0,
+35,Moogle: Semantic search over mathlib4,,cheatsheet,Better performance (latency) than `General Documentation`.,,https://www.moogle.ai/,,,,,,,,,,,,,,,,,,,1,True,3,,,
+36,`#help` command output,,cheatsheet,"Output of `#help option`, `#help attr`, ... shown in `Lean 4 Web`.",,https://live.lean-lang.org/#code=import%20Mathlib.Tactic%0D%0A%0D%0A%23help%20option%0D%0A%23help%20attr%0D%0A%23help%20cats%0D%0A%23help%20term%0D%0A%23help%20tactic%0D%0A%23help%20conv%0D%0A%23help%20command%0D%0A,,,,,,,,,,,,,,,,,,,1,True,3,,,
+37,The Lean Reference Manual,,tutorial,Official Lean 3 Reference Manual.,,https://lean-lang.org/reference/index.html,,,,,,,,,,,,,,,,,,,1,True,3,,,['lean3']
+38,Lean Manual,,tutorial,Official Manual.,,https://lean-lang.org/lean4/doc/do.html,,,,,,,,,,,,,,,,,,,1,True,3,,,
+39,Zulip chat for discussions about Lean and mathlib,,community,Official community.,,https://leanprover.zulipchat.com/,,,,,,,,,,,,,,,,,,,1,True,1,,,
+40,Lean 4 Anarchy (Discord),,community,Anarchy discord server.,,https://discord.com/invite/WZ9bs9UCvx,,,,,,,,,,,,,,,,,,,1,True,1,,,
+41,Links (lean-lang.org),,awesome,Official collection of links.,,https://lean-lang.org/links/,,,,,,,,,,,,,,,,,,,1,True,3,,,
+42,lean4 - Where is the syntax of Lean 4 documented? - Proof Assistants Stack Exchange,,awesome,Discussion regarding Lean 4 documentation.,,https://proofassistants.stackexchange.com/questions/2305/where-is-the-syntax-of-lean-4-documented,,,,,,,,,,,,,,,,,,,1,True,3,,,
+43,lean4 - YouTube,,movie,YouTube movies.,,https://www.youtube.com/results?search_query=lean4,,,,,,,,,,,,,,,,,,,1,True,1,,,
+44,人気の「Lean」動画 14本 - ニコニコ動画,,movie,Niconico movies. Entertaining instructions using TTS software have been uploaded.,,https://www.nicovideo.jp/tag/Lean,,,,,,,,,,,,,,,,,,,1,True,1,,,['ja']
diff --git a/latest-changes.md b/latest-changes.md
index 81b91e0..def7e27 100644
--- a/latest-changes.md
+++ b/latest-changes.md
@@ -2,18 +2,15 @@
_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._
-- elan (🥈21 · ⭐ 320 · 📈) - Version Manager. Apache-2
-- std4 (🥉18 · ⭐ 260 · 📈) - Standard Library. Apache-2
-- Lean Game Server (🥇17 · ⭐ 200 · 📈) - Mainly for Natural Number Game. Be careful not to.. ❗️GPL-3.0
-- Functional Programming in Lean (🥉8 · ⭐ 73 · 💤) - Functional Programming in Lean. ❗Unlicensed
-- lean3-tactic-lean4 (🥈6 · ⭐ 25 · 📈) - Reference sheet for people who know Lean 3 and want.. Unlicense Lean 3
+- doc-gen4 (🥉15 · ⭐ 69 · 📈) - Document Generator. Apache-2
+- Lean 4 Tactics (🥈6 · ⭐ 63 · 📈) - Overview of tactics in Lean 4 for beginners longer version. Unlicense
+- Lean 4 Cheatsheet (🥉5 · ⭐ 23 · 📈) - Printable (A4) overview of tactics in Lean 4 for.. Unlicense
+- (Mathlib4) General Documentation (API Reference) (🥉5 · ⭐ 8 · 📈) - Official Mathlib API Reference. ❗Unlicensed
## 📉 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._
-- LeanDojo (🥈16 · ⭐ 590 · 📉) - Tool for data extraction and interacting with Lean programmatically. MIT
-- Paperproof (🥈16 · ⭐ 370 · 📉) - Theorem proving interface which feels like pen-and-paper proofs. MIT
-- aesop (🥈14 · ⭐ 220 · 📉) - Proof search tactic (Automated Extensible Search for Obvious Proofs). Apache-2
-- lean4web (🥉11 · ⭐ 71 · 📉) - Web editor. Apache-2
-- Mathematics in Lean (🥉10 · ⭐ 280 · 📉) - Note that there are many parts of the documentation.. ❗Unlicensed
+- The mechanics of proof (🥈10 · ⭐ 210 · 📉) - Early university level course. ❗Unlicensed
+- lean4web (🥉10 · ⭐ 73 · 📉) - Web editor. Apache-2
+- Reservoir (🥉7 · ⭐ 17 · 📉) - Lakes package registry. Apache-2