diff --git a/README.md b/README.md index 1da381c..c590638 100644 --- a/README.md +++ b/README.md @@ -59,16 +59,16 @@ This curated list contains 45 awesome open-source projects with a total of 11K s _Quick reference with short text_ -
A mathlib overview (🥇15 · ⭐ 53) - Hosts the website for mathlib and other Lean community.. MIT +
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 · 📋 37 - 59% open · ⏱️ 04.11.2024): +- [GitHub](https://github.com/leanprover-community/leanprover-community.github.io) (👨‍💻 120 · 🔀 120 · 📋 38 - 57% open · ⏱️ 26.11.2024): ``` git clone https://github.com/leanprover-community/leanprover-community.github.io ```
-
Lean 4 Tactics (🥈6 · ⭐ 57 · 📉) - Overview of tactics in Lean 4 for beginners longer version. Unlicense +
Lean 4 Tactics (🥈6 · ⭐ 59) - Overview of tactics in Lean 4 for beginners longer version. Unlicense - [GitHub](https://github.com/madvorak/lean4-tactics) (👨‍💻 2 · 🔀 2 · ⏱️ 19.09.2024): @@ -77,25 +77,25 @@ _Quick reference with short text_ ```
-
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 ```
-
lean3-tactic-lean4 (🥉5 · ⭐ 24) - Reference sheet for people who know Lean 3 and want.. Unlicense Lean 3 +
Lean by Example (🥈6) - Lean. MIT ja -- [GitHub](https://github.com/madvorak/lean3-tactic-lean4) (👨‍💻 2 · 🔀 2 · ⏱️ 13.10.2024): +- [GitHub](https://github.com/lean-ja/lean-ja.github.io) (👨‍💻 3 · ⏱️ 18.06.2024): ``` - git clone https://github.com/madvorak/lean3-tactic-lean4 + git clone https://github.com/lean-ja/lean-ja.github.io ```
-
Lean 4 Cheatsheet (🥉4 · ⭐ 20) - Printable (A4) overview of tactics in Lean 4 for beginners. Unlicense +
Lean 4 Cheatsheet (🥉5 · ⭐ 21 · 📈) - Printable (A4) overview of tactics in Lean 4 for.. Unlicense - [GitHub](https://github.com/madvorak/lean4-cheatsheet) (🔀 1 · ⏱️ 19.09.2024): @@ -131,9 +131,9 @@ _Quick reference with short text_ _Tutorials with long text_ -
A Lean 4 Metaprogramming Book (🥇15 · ⭐ 220 · 📉) - Practical manual with code that goes into the.. Apache-2 +
A Lean 4 Metaprogramming Book (🥇15 · ⭐ 220) - Practical manual with code that goes into the.. Apache-2 -- [GitHub](https://github.com/leanprover-community/lean4-metaprogramming-book) (👨‍💻 24 · 🔀 54 · 📥 12 · 📋 39 - 43% open · ⏱️ 05.11.2024): +- [GitHub](https://github.com/leanprover-community/lean4-metaprogramming-book) (👨‍💻 24 · 🔀 55 · 📥 78 · 📋 39 - 43% open · ⏱️ 05.11.2024): ``` git clone https://github.com/leanprover-community/lean4-metaprogramming-book @@ -142,34 +142,34 @@ _Tutorials with long text_
Theorem Proving in Lean 4 (🥈12 · ⭐ 160) - Theorem Proving in Lean 4. Apache-2 -- [GitHub](https://github.com/leanprover/theorem_proving_in_lean4) (👨‍💻 80 · 🔀 88 · 📋 39 - 66% open · ⏱️ 14.10.2024): +- [GitHub](https://github.com/leanprover/theorem_proving_in_lean4) (👨‍💻 80 · 🔀 89 · 📋 42 - 69% open · ⏱️ 14.10.2024): ``` git clone https://github.com/leanprover/theorem_proving_in_lean4 ```
-
Mathematics in Lean (🥈11 · ⭐ 260) - Note that there are many parts of the documentation.. ❗Unlicensed +
The mechanics of proof (🥈11 · ⭐ 210) - Early university level course. ❗Unlicensed -- [GitHub](https://github.com/leanprover-community/mathematics_in_lean) (👨‍💻 3 · 🔀 190 · ⏱️ 21.10.2024): +- [GitHub](https://github.com/hrmacbeth/math2001) (🔀 79 · 📋 17 - 58% open · ⏱️ 24.11.2024): ``` - git clone https://github.com/leanprover-community/mathematics_in_lean + git clone https://github.com/hrmacbeth/math2001 ```
-
The mechanics of proof (🥈11 · ⭐ 200 · 📈) - Early university level course. ❗Unlicensed +
Mathematics in Lean (🥉10 · ⭐ 280 · 📉) - Note that there are many parts of the documentation.. ❗Unlicensed -- [GitHub](https://github.com/hrmacbeth/math2001) (🔀 77 · 📋 16 - 56% open · ⏱️ 01.11.2024): +- [GitHub](https://github.com/leanprover-community/mathematics_in_lean) (👨‍💻 3 · 🔀 190 · ⏱️ 11.11.2024): ``` - git clone https://github.com/hrmacbeth/math2001 + git clone https://github.com/leanprover-community/mathematics_in_lean ```
Functional Programming in Lean (🥉7 · ⭐ 71 · 💤) - Functional Programming in Lean. ❗Unlicensed -- [GitHub](https://github.com/leanprover/fp-lean) (👨‍💻 2 · 🔀 20 · 📥 73 · 📋 150 - 33% open · ⏱️ 06.02.2024): +- [GitHub](https://github.com/leanprover/fp-lean) (👨‍💻 2 · 🔀 20 · 📥 73 · 📋 160 - 34% open · ⏱️ 06.02.2024): ``` git clone https://github.com/leanprover/fp-lean @@ -192,7 +192,7 @@ _Actual Lean 4 code for learning purposes_
Lean Math Workshop (🥇10 · ⭐ 69) - Materials for a workshop held in Japan. Apache-2 ja -- [GitHub](https://github.com/yuma-mizuno/lean-math-workshop) (👨‍💻 5 · 🔀 22 · 📋 13 - 7% open · ⏱️ 13.07.2024): +- [GitHub](https://github.com/yuma-mizuno/lean-math-workshop) (👨‍💻 5 · 🔀 22 · 📋 14 - 14% open · ⏱️ 13.07.2024): ``` git clone https://github.com/yuma-mizuno/lean-math-workshop @@ -201,7 +201,7 @@ _Actual Lean 4 code for learning purposes_
The Matrix Cookbook, using Lean's mathlib (🥉7 · ⭐ 84) - The matrix cookbook, proved in the Lean theorem prover. MIT -- [GitHub](https://github.com/eric-wieser/lean-matrix-cookbook) (👨‍💻 2 · 🔀 11 · ⏱️ 02.10.2024): +- [GitHub](https://github.com/eric-wieser/lean-matrix-cookbook) (👨‍💻 2 · 🔀 11 · ⏱️ 23.11.2024): ``` git clone https://github.com/eric-wieser/lean-matrix-cookbook @@ -216,9 +216,9 @@ _Actual Lean 4 code for learning purposes_ _Reusable Lean 4 code for enhancing usability_ -
ProofWidgets (🥇19 · ⭐ 110) - Helper toolkit for creating your own Lean 4 UserWidgets. Apache-2 +
ProofWidgets (🥇19 · ⭐ 120) - Helper toolkit for creating your own Lean 4 UserWidgets. Apache-2 -- [GitHub](https://github.com/leanprover-community/ProofWidgets4) (👨‍💻 14 · 🔀 26 · 📥 360K · 📋 20 - 65% open · ⏱️ 04.11.2024): +- [GitHub](https://github.com/leanprover-community/ProofWidgets4) (👨‍💻 14 · 🔀 26 · 📥 380K · 📋 21 - 61% open · ⏱️ 24.11.2024): ``` git clone https://github.com/leanprover-community/ProofWidgets4 @@ -242,34 +242,34 @@ _Reusable Lean 4 code for enhancing usability_ _Reusable Lean 4 code (theorems, etc.)_ -
SciLean (🥇15 · ⭐ 320) - Scientific computing in Lean 4. Apache-2 +
SciLean (🥇15 · ⭐ 330) - Scientific computing in Lean 4. Apache-2 -- [GitHub](https://github.com/lecopivo/SciLean) (👨‍💻 9 · 🔀 29 · 📋 34 - 55% open · ⏱️ 07.11.2024): +- [GitHub](https://github.com/lecopivo/SciLean) (👨‍💻 9 · 🔀 30 · 📋 37 - 54% open · ⏱️ 27.11.2024): ``` git clone https://github.com/lecopivo/SciLean ```
-
aesop (🥇15 · ⭐ 210) - Proof search tactic (Automated Extensible Search for Obvious Proofs). Apache-2 +
aesop (🥈14 · ⭐ 210 · 📉) - Proof search tactic (Automated Extensible Search for Obvious Proofs). Apache-2 -- [GitHub](https://github.com/leanprover-community/aesop) (👨‍💻 20 · 🔀 28 · 📋 63 - 34% open · ⏱️ 06.11.2024): +- [GitHub](https://github.com/leanprover-community/aesop) (👨‍💻 20 · 🔀 28 · 📋 64 - 34% open · ⏱️ 14.11.2024): ``` git clone https://github.com/leanprover-community/aesop ```
-
SMT Lean (🥈10 · ⭐ 100) - Tactics for discharging Lean goals into SMT solvers. Apache-2 +
SMT Lean (🥈10 · ⭐ 140) - Tactics for discharging Lean goals into SMT solvers. Apache-2 -- [GitHub](https://github.com/ufmg-smite/lean-smt) (👨‍💻 8 · 🔀 20 · 📋 17 - 47% open · ⏱️ 26.10.2024): +- [GitHub](https://github.com/ufmg-smite/lean-smt) (👨‍💻 8 · 🔀 19 · 📋 17 - 47% open · ⏱️ 27.11.2024): ``` git clone https://github.com/ufmg-smite/lean-smt ```
-
CvxLean (🥈10 · ⭐ 40) - Convex optimization modeling in Lean 4. Apache-2 +
CvxLean (🥈10 · ⭐ 41) - Convex optimization modeling in Lean 4. Apache-2 - [GitHub](https://github.com/verified-optimization/CvxLean) (👨‍💻 3 · 🔀 4 · ⏱️ 20.05.2024): @@ -306,25 +306,25 @@ _Core Lean 4 code_
lean4 (🥇32 · ⭐ 4.7K) - Lean 4 repository. Includes `Lake`. Apache-2 -- [GitHub](https://github.com/leanprover/lean4) (👨‍💻 200 · 🔀 420 · 📥 450K · 📋 1.9K - 30% open · ⏱️ 07.11.2024): +- [GitHub](https://github.com/leanprover/lean4) (👨‍💻 210 · 🔀 420 · 📥 500K · 📋 2K - 30% open · ⏱️ 28.11.2024): ``` git clone https://github.com/leanprover/lean4 ```
-
mathlib4 (🥈25 · ⭐ 1.5K) - Math library. Apache-2 +
mathlib4 (🥈25 · ⭐ 1.6K) - Math library. Apache-2 -- [GitHub](https://github.com/leanprover-community/mathlib4) (👨‍💻 360 · 🔀 330 · 📋 410 - 55% open · ⏱️ 07.11.2024): +- [GitHub](https://github.com/leanprover-community/mathlib4) (👨‍💻 370 · 🔀 330 · 📋 420 - 55% open · ⏱️ 28.11.2024): ``` git clone https://github.com/leanprover-community/mathlib4 ```
-
elan (🥈20 · ⭐ 320 · 📈) - Version Manager. Apache-2 +
elan (🥈21 · ⭐ 320 · 📈) - Version Manager. Apache-2 -- [GitHub](https://github.com/leanprover/elan) (👨‍💻 21 · 🔀 35 · 📥 830K · 📋 75 - 32% open · ⏱️ 06.11.2024): +- [GitHub](https://github.com/leanprover/elan) (👨‍💻 22 · 🔀 36 · 📥 870K · 📋 77 - 33% open · ⏱️ 26.11.2024): ``` git clone https://github.com/leanprover/elan @@ -333,16 +333,16 @@ _Core Lean 4 code_
std4 (🥉16 · ⭐ 250) - Standard Library. Apache-2 -- [GitHub](https://github.com/leanprover-community/batteries) (👨‍💻 62 · 🔀 100 · 📋 61 - 37% open · ⏱️ 05.11.2024): +- [GitHub](https://github.com/leanprover-community/batteries) (👨‍💻 63 · 🔀 100 · 📋 62 - 33% open · ⏱️ 27.11.2024): ``` git clone https://github.com/leanprover/std4 ```
-
doc-gen4 (🥉14 · ⭐ 65) - Document Generator. Apache-2 +
doc-gen4 (🥉14 · ⭐ 67) - Document Generator. Apache-2 -- [GitHub](https://github.com/leanprover/doc-gen4) (👨‍💻 31 · 🔀 41 · 📋 82 - 34% open · ⏱️ 04.11.2024): +- [GitHub](https://github.com/leanprover/doc-gen4) (👨‍💻 32 · 🔀 42 · 📋 83 - 30% open · ⏱️ 20.11.2024): ``` git clone https://github.com/leanprover/doc-gen4 @@ -366,9 +366,9 @@ _Core Lean 4 code_ _Lean 4 Games_ -
Lean Game Server (🥇16 · ⭐ 190) - Mainly for Natural Number Game. Be careful not to.. ❗️GPL-3.0 +
Lean Game Server (🥇16 · ⭐ 200) - Mainly for Natural Number Game. Be careful not to.. ❗️GPL-3.0 -- [GitHub](https://github.com/leanprover-community/lean4game) (👨‍💻 20 · 🔀 33 · 📋 230 - 32% open · ⏱️ 25.10.2024): +- [GitHub](https://github.com/leanprover-community/lean4game) (👨‍💻 20 · 🔀 34 · 📋 230 - 32% open · ⏱️ 25.11.2024): ``` git clone https://github.com/leanprover-community/lean4game @@ -399,34 +399,34 @@ _Tools not made in Lean 4_
vscode-lean4 (🥇20 · ⭐ 170) - Visual Studio Code extension. Apache-2 -- [GitHub](https://github.com/leanprover/vscode-lean4) (👨‍💻 58 · 🔀 48 · 📥 440 · 📋 210 - 21% open · ⏱️ 06.11.2024): +- [GitHub](https://github.com/leanprover/vscode-lean4) (👨‍💻 58 · 🔀 49 · 📥 450 · 📋 210 - 20% open · ⏱️ 20.11.2024): ``` git clone https://github.com/leanprover/vscode-lean4 ```
-
LeanDojo (🥈17 · ⭐ 570) - Tool for data extraction and interacting with Lean programmatically. MIT +
LeanDojo (🥈17 · ⭐ 580) - Tool for data extraction and interacting with Lean programmatically. MIT -- [GitHub](https://github.com/lean-dojo/LeanDojo) (👨‍💻 17 · 🔀 89 · 📋 64 - 7% open · ⏱️ 13.10.2024): +- [GitHub](https://github.com/lean-dojo/LeanDojo) (👨‍💻 17 · 🔀 93 · 📋 64 - 4% open · ⏱️ 13.10.2024): ``` git clone https://github.com/lean-dojo/LeanDojo ```
-
Paperproof (🥈17 · ⭐ 360) - Theorem proving interface which feels like pen-and-paper proofs. MIT +
Paperproof (🥈17 · ⭐ 370) - Theorem proving interface which feels like pen-and-paper proofs. MIT -- [GitHub](https://github.com/Paper-Proof/paperproof) (👨‍💻 5 · 🔀 9 · 📋 34 - 32% open · ⏱️ 04.11.2024): +- [GitHub](https://github.com/Paper-Proof/paperproof) (👨‍💻 5 · 🔀 10 · 📋 34 - 32% open · ⏱️ 13.11.2024): ``` git clone https://github.com/Paper-Proof/paperproof ```
-
lean4web (🥉13 · ⭐ 68) - Web editor. Apache-2 +
lean4web (🥉11 · ⭐ 68 · 📉) - Web editor. Apache-2 -- [GitHub](https://github.com/leanprover-community/lean4web) (👨‍💻 6 · 🔀 19 · 📋 36 - 19% open · ⏱️ 23.09.2024): +- [GitHub](https://github.com/leanprover-community/lean4web) (👨‍💻 7 · 🔀 19 · 📋 37 - 21% open · ⏱️ 24.11.2024): ``` git clone https://github.com/leanprover-community/lean4web diff --git a/history/2024-11-28_changes.md b/history/2024-11-28_changes.md new file mode 100644 index 0000000..dc01436 --- /dev/null +++ b/history/2024-11-28_changes.md @@ -0,0 +1,15 @@ +## 📈 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._ + +- elan (🥈21 · ⭐ 320 · 📈) - Version Manager. Apache-2 +- lean3-tactic-lean4 (🥈6 · ⭐ 25 · 📈) - Reference sheet for people who know Lean 3 and want.. Unlicense Lean 3 +- Lean 4 Cheatsheet (🥉5 · ⭐ 21 · 📈) - Printable (A4) overview of tactics in Lean 4 for.. Unlicense + +## 📉 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._ + +- aesop (🥈14 · ⭐ 210 · 📉) - Proof search tactic (Automated Extensible Search for Obvious Proofs). Apache-2 +- lean4web (🥉11 · ⭐ 68 · 📉) - Web editor. Apache-2 +- Mathematics in Lean (🥉10 · ⭐ 280 · 📉) - Note that there are many parts of the documentation.. ❗Unlicensed diff --git a/history/2024-11-28_projects.csv b/history/2024-11-28_projects.csv new file mode 100644 index 0000000..2d9ed77 --- /dev/null +++ b/history/2024-11-28_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,trending,updated_github_id,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-11-28 17:37:38,2024-11-28 05:23:23,34524.0,750.0,424.0,63.0,4265.0,597.0,1371.0,4749.0,2024-11-01 02:36:33,4.13.0,495370.0,10768.0,56.0,207.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-11-28 18:07:49,2024-11-28 17:43:16,16331.0,2744.0,333.0,38.0,19152.0,233.0,186.0,1569.0,,,,,,366.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-11-26 09:33:29,2024-11-26 09:32:56,329.0,12.0,36.0,15.0,69.0,26.0,51.0,321.0,2024-02-22 22:04:49,3.1.1,872711.0,11046.0,58.0,22.0,21,True,2,1.0,, +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-11-28 16:45:02,2024-11-20 15:00:14,2646.0,33.0,49.0,11.0,333.0,42.0,166.0,170.0,2024-10-28 10:39:11,0.0.184,450.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-11-27 10:59:20,2024-11-24 03:02:05,336.0,40.0,26.0,8.0,69.0,13.0,8.0,116.0,2024-11-27 11:00:59,0.0.47-pre,381500.0,17340.0,68.0,14.0,19,True,1,,, +5,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-10-13 22:39:07,2024-10-13 22:35:35,589.0,10.0,93.0,13.0,119.0,3.0,61.0,576.0,2024-10-13 22:39:07,2.1.3,,,33.0,17.0,17,True,2,,, +6,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,47.0,10.0,7.0,17.0,11.0,23.0,368.0,2024-11-04 14:22:09,1.6.4,,,4.0,5.0,17,True,2,,, +7,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-11-28 14:49:08,2024-11-27 11:33:25,979.0,112.0,105.0,16.0,1003.0,21.0,41.0,253.0,,,,,,63.0,16,True,3,,leanprover-community/batteries, +8,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-11-25 11:38:19,2024-11-25 11:38:16,1063.0,21.0,34.0,10.0,44.0,75.0,154.0,198.0,2024-04-10 13:24:11,4.7.0,,,10.0,20.0,16,True,1,,, +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-11-27 22:47:24,2024-11-27 22:46:49,1813.0,105.0,30.0,19.0,12.0,20.0,17.0,333.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,225.0,,,78.0,78.0,1.0,24.0,15,True,1,,, +11,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-11-28 04:08:05,2024-11-26 18:08:28,10253.0,38.0,123.0,12.0,519.0,22.0,16.0,55.0,,,,,,119.0,15,True,1,,, +12,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-11-28 16:00:20,2024-11-14 02:55:40,809.0,37.0,28.0,9.0,115.0,22.0,42.0,214.0,,,,,,20.0,14,True,2,-1.0,, +13,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-11-20 13:55:39,2024-11-20 13:55:39,554.0,34.0,42.0,12.0,154.0,25.0,58.0,67.0,,,,,,32.0,14,True,3,,, +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,89.0,11.0,98.0,29.0,13.0,164.0,,,,,,80.0,12,True,2,,, +15,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-11-24 16:16:35,2024-11-24 16:16:32,269.0,12.0,79.0,3.0,9.0,10.0,7.0,206.0,,,,,,,11,True,2,,, +16,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,7.0,19.0,10.0,9.0,8.0,29.0,68.0,,,,,,7.0,11,True,3,-2.0,, +17,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-11-11 09:26:12,2024-11-11 09:26:08,80.0,6.0,193.0,14.0,19.0,,,275.0,,,,,,3.0,10,True,3,-1.0,, +18,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-11-27 16:17:06,2024-11-27 16:17:02,134.0,26.0,19.0,9.0,135.0,8.0,9.0,145.0,,,,,,8.0,10,True,2,,, +19,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-11-04 01:45:15,2024-11-04 01:44:42,171.0,7.0,12.0,6.0,43.0,13.0,9.0,75.0,,,,,,8.0,10,True,3,,, +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,69.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,,41.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,4.0,18.0,3.0,2.0,119.0,2023-10-31 03:18:38,1.0.0,,,1.0,5.0,8,True,3,,, +23,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,1.0,3.0,6.0,14.0,1.0,,42.0,,,,,,3.0,8,True,3,,, +24,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,12.0,1.0,3.0,31.0,5.0,19.0,16.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,4.0,14.0,,2.0,84.0,,,,,,2.0,7,True,3,,, +26,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,,20.0,5.0,18.0,53.0,102.0,71.0,2022-11-27 19:58:21,pre-2022-11,73.0,2.0,5.0,2.0,7,True,3,,, +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,1.0,2.0,4.0,1.0,,,59.0,,,,,,2.0,6,True,2,,, +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,1.0,,['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,1.0,,,,21.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-10-06 17:43:49,2024-10-06 17:43:44,21.0,5.0,2.0,19.0,2.0,,1.0,8.0,,,,,,4.0,4,True,3,,, +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 324c495..dc01436 100644 --- a/latest-changes.md +++ b/latest-changes.md @@ -2,12 +2,14 @@ _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 (🥈20 · ⭐ 320 · 📈) - Version Manager. Apache-2 -- The mechanics of proof (🥈11 · ⭐ 200 · 📈) - Early university level course. ❗Unlicensed +- elan (🥈21 · ⭐ 320 · 📈) - Version Manager. Apache-2 +- lean3-tactic-lean4 (🥈6 · ⭐ 25 · 📈) - Reference sheet for people who know Lean 3 and want.. Unlicense Lean 3 +- Lean 4 Cheatsheet (🥉5 · ⭐ 21 · 📈) - Printable (A4) overview of tactics in Lean 4 for.. Unlicense ## 📉 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._ -- A Lean 4 Metaprogramming Book (🥇15 · ⭐ 220 · 📉) - Practical manual with code that goes into the.. Apache-2 -- Lean 4 Tactics (🥈6 · ⭐ 57 · 📉) - Overview of tactics in Lean 4 for beginners longer version. Unlicense +- aesop (🥈14 · ⭐ 210 · 📉) - Proof search tactic (Automated Extensible Search for Obvious Proofs). Apache-2 +- lean4web (🥉11 · ⭐ 68 · 📉) - Web editor. Apache-2 +- Mathematics in Lean (🥉10 · ⭐ 280 · 📉) - Note that there are many parts of the documentation.. ❗Unlicensed