Lean

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.

    Project mention: Leantime: Project Management System for People with ADHD | news.ycombinator.com | 2024-01-29
  • lean4

    Lean 4 programming language and theorem prover

    Project mention: The Mechanics of Proof | news.ycombinator.com | 2024-03-20
  • 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.

  • mathlib

    Lean 3's obsolete mathematical components library: please use mathlib4

    Project mention: An Easy-Sounding Problem Yields Numbers Too Big for Our Universe | news.ycombinator.com | 2023-12-04
  • awesome-agile

    Awesome List of resources on Agile Software Development.

  • LeanCopilot

    LLMs as Copilots for Theorem Proving in Lean

    Project mention: LeanDojo: Theorem Proving with Retrieval-Augmented Language Models | /r/math | 2023-12-11
  • parsel

    Code for Parsel 🐍 - generate complex programs with language models (by ezelikman)

  • std4

    Standard Library for Lean 4

    Project mention: The Mechanics of Proof | news.ycombinator.com | 2024-03-20
  • 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.

  • LeanDojoChatGPT

    ChatGPT plugin for theorem proving in Lean

    Project mention: 'A-Team' of Math Proves a Critical Link Between Addition and Sets | news.ycombinator.com | 2023-12-08

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

  • hott3

    HoTT in Lean 3

  • 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: Starting Design Work in a Spreadsheet | news.ycombinator.com | 2023-07-05

    I love spreadsheets! I start with a design doc which usually contains tables in my process: https://github.com/ryanallen/designDoc

  • trepplein

    Lean type-checker written in Scala.

  • eAndon

    Implementation of an electronic Andon system to visualize problems in a production company.

NOTE: The open source projects on this list are ordered by number of github stars. The number of mentions indicates repo mentiontions in the last 12 Months or since we started tracking (Dec 2020). The latest post mention was on 2024-03-20.

Lean related posts

Index

What are some of the best open-source Lean projects? This list will help you:

Project Stars
1 Leantime 4,037
2 lean4 3,687
3 mathlib 1,619
4 awesome-agile 1,275
5 LeanCopilot 659
6 parsel 371
7 std4 190
8 LeanDojoChatGPT 98
9 hott3 72
10 designDoc 42
11 trepplein 26
12 eAndon 6
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com