The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning. Learn more →
Top 12 Lean Open-Source Projects
-
Leantime
Leantime is a goals focused project management system for non-project managers. Building with ADHD, Autism, and dyslexia in mind.
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
-
WorkOS
The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
-
designDoc
A lean product design process in markdown that enables cross-functional teams to take an idea from napkin to scale by prioritizing learnings to produce customer-centered solutions.
Project mention: Leantime: Project Management System for People with ADHD | news.ycombinator.com | 2024-01-29
Project mention: Dafny is a verification-aware programming language | news.ycombinator.com | 2024-04-23Recently replaced by Lean, though.
https://github.com/cedar-policy/cedar-spec
https://lean-lang.org
Project mention: An Easy-Sounding Problem Yields Numbers Too Big for Our Universe | news.ycombinator.com | 2023-12-04
Project mention: New Foundations is consistent – a difficult mathematical proof proved using Lean | news.ycombinator.com | 2024-04-23Then it's time to update your LLM reading!
https://leandojo.org/
Project mention: 'A-Team' of Math Proves a Critical Link Between Addition and Sets | news.ycombinator.com | 2023-12-08Check out this paper:
https://leandojo.org/
People have already trained models to assist suggestion tactics. They then linked it up to ChatGPT to interactively solve proofs.
In this scenario, ChatGPT asks the model for tactic suggestions, applies it to the proof and uses the feedback from Lean to then proceed with the next step.
FYI, The programmatic interface to Lean was written by an OpenAI employee who was on the Lean team a few years ago.
Also, check out Lean’s roadmap. They aspire to position Lean to becoming a target for LLMs because it has been designed for verification from the ground up.
As math and compsci nerds contribute to mathlib, all of those proofs are also building up a huge corpus that will likely be leveraged for both verification and optimization.
If AI can make verification a lot easier, then we’re likely going to see verification change programming similarly to the way it changed electronics.
I love spreadsheets! I start with a design doc which usually contains tables in my process: https://github.com/ryanallen/designDoc
Lean related posts
- Dafny is a verification-aware programming language
- New Foundations is consistent – a difficult mathematical proof proved using Lean
- The Mechanics of Proof
- Natural Deduction in Logic (2015)
- LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
- LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
- The Wizardry Frontier
-
A note from our sponsor - WorkOS
workos.com | 29 Apr 2024
Index
What are some of the best open-source Lean projects? This list will help you:
Project | Stars | |
---|---|---|
1 | Leantime | 4,059 |
2 | lean4 | 3,739 |
3 | mathlib | 1,625 |
4 | awesome-agile | 1,275 |
5 | LeanCopilot | 796 |
6 | parsel | 375 |
7 | std4 | 195 |
8 | LeanDojoChatGPT | 98 |
9 | hott3 | 72 |
10 | designDoc | 42 |
11 | trepplein | 26 |
12 | eAndon | 6 |
Sponsored