+ 
-
+
MITUnlicense Lean 3UnlicenseMIT jaUnlicense Lean 3UnlicenseMIT jaUnlicenseUnlicense❗Unlicensed❗UnlicensedApache-2Apache-2❗Unlicensed❗Unlicensed❗Unlicensed❗UnlicensedApache-2 jaApache-2 jaMITMITApache-2Apache-2Apache-2Apache-2Apache-2Apache-2Apache-2Apache-2Apache-2Apache-2Apache-2Apache-2Apache-2Apache-2Apache-2Apache-2Apache-2Apache-2Apache-2Apache-2Apache-2❗️GPL-3.0❗️GPL-3.0Apache-2MITMITMITMITMITApache-2Apache-2Apache-2Apache-2Apache-2
+- SMT Lean (🥈11 · ⭐ 150 · 📈) - Tactics for discharging Lean goals into SMT solvers. 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
+
+## ➕ Added Projects
+
+_Projects that were recently added to this best-of list._
+
+- LeanCopilot (🥈17 · ⭐ 1K · ➕) - LLMs as Copilots for Theorem Proving in Lean. MIT
diff --git a/history/2024-12-19_projects.csv b/history/2024-12-19_projects.csv
new file mode 100644
index 0000000..74bb3bb
--- /dev/null
+++ b/history/2024-12-19_projects.csv
@@ -0,0 +1,47 @@
+,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,new_addition,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 23:45:01,2024-12-19 20:15:49,34658.0,737.0,429.0,64.0,4405.0,608.0,1391.0,4826.0,2024-12-01 23:57:48,4.14.0,536676.0,11418.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 23:53:26,2024-12-19 21:50:31,16724.0,2619.0,342.0,36.0,19665.0,238.0,188.0,1622.0,,,,,,374.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,37.0,16.0,74.0,26.0,51.0,326.0,2024-02-22 22:04:49,3.1.1,912639.0,11407.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,482.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-19 09:44:10,2024-12-12 16:36:39,345.0,37.0,28.0,8.0,74.0,15.0,9.0,119.0,2024-12-19 09:45:42,0.0.49-pre1,397272.0,17272.0,71.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 18:30:44,2024-12-12 13:17:51,987.0,103.0,108.0,16.0,1013.0,20.0,42.0,257.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,LeanCopilot,lean-dojo/LeanCopilot,tool,LLMs as Copilots for Theorem Proving in Lean.,https://github.com/lean-dojo/LeanCopilot,https://github.com/lean-dojo/LeanCopilot,MIT,2023-09-09 01:52:22,2024-11-04 01:35:17,2024-11-04 01:33:05,696.0,2.0,92.0,15.0,77.0,11.0,34.0,1009.0,2024-09-02 09:55:55,1.6.0,3156.0,210.0,31.0,11.0,17,True,2,,True,,
+7,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,36.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,,,,
+8,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,,,,
+9,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,,,,
+10,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,347.0,,,,,,9.0,15,True,1,,,,
+11,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,,,146.0,146.0,1.0,24.0,15,True,1,,,,
+12,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,167.0,23.0,62.0,69.0,,,,,,33.0,15,True,3,,,1.0,
+13,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 16:31:39,2024-12-19 15:37:22,10257.0,35.0,123.0,12.0,524.0,22.0,16.0,55.0,,,,,,119.0,15,True,1,,,,
+14,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-19 09:58:51,2024-12-19 09:54:36,814.0,19.0,28.0,9.0,121.0,22.0,42.0,221.0,,,,,,20.0,14,True,2,,,,
+15,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,,,,
+16,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 21:57:08,2024-12-17 06:37:21,137.0,29.0,19.0,9.0,140.0,8.0,9.0,149.0,,,,,,8.0,11,True,2,,,1.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-12-02 15:39:14,2024-12-02 15:39:32,81.0,6.0,193.0,14.0,19.0,,,286.0,,,,,,3.0,10,True,2,,,,
+18,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,
+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-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,,,,
+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,74.0,,,,,,5.0,10,True,1,,,,['ja']
+21,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,
+22,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,3,,,,
+23,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,,,,
+24,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,,,,
+25,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,,,,
+26,"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,,,,
+27,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,
+28,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,
+29,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,,,,
+30,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']
+31,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']
+32,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']
+33,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']
+34,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,
+35,(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,
+36,Moogle: Semantic search over mathlib4,,cheatsheet,Better performance (latency) than `General Documentation`.,,https://www.moogle.ai/,,,,,,,,,,,,,,,,,,,1,True,3,,,,
+37,`#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,,,,
+38,The Lean Reference Manual,,tutorial,Official Lean 3 Reference Manual.,,https://lean-lang.org/reference/index.html,,,,,,,,,,,,,,,,,,,1,True,3,,,,['lean3']
+39,Lean Manual,,tutorial,Official Manual.,,https://lean-lang.org/lean4/doc/do.html,,,,,,,,,,,,,,,,,,,1,True,3,,,,
+40,Zulip chat for discussions about Lean and mathlib,,community,Official community.,,https://leanprover.zulipchat.com/,,,,,,,,,,,,,,,,,,,1,True,1,,,,
+41,Lean 4 Anarchy (Discord),,community,Anarchy discord server.,,https://discord.com/invite/WZ9bs9UCvx,,,,,,,,,,,,,,,,,,,1,True,1,,,,
+42,Links (lean-lang.org),,awesome,Official collection of links.,,https://lean-lang.org/links/,,,,,,,,,,,,,,,,,,,1,True,3,,,,
+43,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,,,,
+44,lean4 - YouTube,,movie,YouTube movies.,,https://www.youtube.com/results?search_query=lean4,,,,,,,,,,,,,,,,,,,1,True,1,,,,
+45,人気の「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..0d052ac 100644
--- a/latest-changes.md
+++ b/latest-changes.md
@@ -2,18 +2,22 @@
_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
+- SMT Lean (🥈11 · ⭐ 150 · 📈) - Tactics for discharging Lean goals into SMT solvers. 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
+
+## ➕ Added Projects
+
+_Projects that were recently added to this best-of list._
+
+- LeanCopilot (🥈17 · ⭐ 1K · ➕) - LLMs as Copilots for Theorem Proving in Lean. MIT