Update: 2024.06.27

📈 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 · ⭐ 270 · 📈) - Version Manager. Apache-2
• vscode-lean4 (🥇20 · ⭐ 140 · 📈) - Visual Studio Code extension. Apache-2
• ProofWidgets (🥇20 · ⭐ 93 · 📈) - Helper toolkit for creating your own Lean 4 UserWidgets. Apache-2
• lean3-tactic-lean4 (🥈5 · ⭐ 21 · 📈) - Reference sheet for people who know Lean 3 and want.. Unlicense Lean 3

📉 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.

• Lean Game Server (🥇16 · ⭐ 130 · 📉) - Mainly for Natural Number Game. Be careful not to.. ❗️GPL-3.0

Update: 2024.06.22-12.37

Nothing changed from last update.

Update: 2024.06.22-11.09

Nothing changed from last update.

Update: 2024.06.22-08.02

Nothing changed from last update.

Update: 2024.06.22-07.58

Nothing changed from last update.

Update: 2024.06.22-07.56

Nothing changed from last update.

Update: 2024.06.22

📈 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.

• mathlib4 (🥈25 · ⭐ 1.1K · 📈) - Math library. Apache-2
• elan (🥈20 · ⭐ 270 · 📈) - Version Manager. Apache-2
• ProofWidgets (🥇19 · ⭐ 92 · 📈) - Helper toolkit for creating your own Lean 4 UserWidgets. Apache-2
• Lean Game Server (🥇17 · ⭐ 130 · 📈) - Mainly for Natural Number Game. Be careful not to.. ❗️GPL-3.0
• aesop (🥇15 · ⭐ 150 · 📈) - Proof search tactic (Automated Extensible Search for Obvious Proofs). Apache-2

📉 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.

• SciLean (🥈14 · ⭐ 240 · 📉) - Scientific computing in Lean 4. Apache-2
• CvxLean (🥈12 · ⭐ 28 · 📉) - Convex optimization modeling in Lean 4. Apache-2
• Theorem Proving in Lean 4 (🥈11 · ⭐ 140 · 📉) - Theorem Proving in Lean 4. Apache-2
• SATurn (🥉6 · ⭐ 50 · 📉) - Experiments with SAT solvers with proofs in Lean 4. MIT

Update: 2024.02.09

📈 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.

• Paperproof (🥉17 · ⭐ 260 · 📈) - Theorem proving interface which feels like pen-and-paper proofs. MIT
• std4 (🥉17 · ⭐ 170 · 📈) - Standard Library. Apache-2
• A Lean 4 Metaprogramming Book (🥇16 · ⭐ 190 · 📈) - Practical manual with code that goes into the.. Apache-2
• The mechanics of proof (🥈10 · ⭐ 73 · 📈) - Early university level course. ❗Unlicensed
• Lean Math Workshop (🥇10 · ⭐ 48 · 📈) - Materials for a workshop held in Japan. Apache-2 ja

📉 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.

• SciLean (🥇14 · ⭐ 180 · 📉) - Scientific computing in Lean 4. Apache-2
• llmstep (🥉9 · ⭐ 80 · 📉) - llmstep: [L]LM proofstep suggestions in Lean 4. MIT
• cs-dm/CheatSheet.lean (🥈6 · ⭐ 15 · 💀) - CS2012 UVa CS Discrete Math Spring 2018. ❗Unlicensed Lean 3
• Lean 4 Tactics Reverse Lookup List (🥈5 · 🐣) - Lean 4 Tactics Reverse Lookup List. MIT ja
• LEAN JA リンク集 (🥇5 · 🐣) - Japanese translated versions of several tutorials are available. (). MIT ja

➕ Added Projects

Projects that were recently added to this best-of list.

• CvxLean (🥈11 · ⭐ 20 · ➕) - Convex optimization modeling in Lean 4. Apache-2