leanprover
Lean Joined Apr 2014 View on GitHub
- Stars
- 18,054
- across 213 public repos
- Rank
- #2,086
- of 94,827 organizations, top 3%
Repositories with 50+ stars
| Rank | Repository | Language | Stars |
|---|---|---|---|
| 5,787 | Lean 4 programming language and theorem prover | Lean | 9,937 |
| 31,628 | Lean Theorem Prover | C++ | 2,151 |
| 81,379 | The Lean Computer Science Library (CSLib) | Lean | 802 |
| 94,989 | The Lean version manager | Rust | 678 |
| 150,426 | Lean documentation authoring tool | Lean | 407 |
| 187,283 | VS Code extension for the Lean 4 programming language and theorem prover | TypeScript | 317 |
| 202,798 | Theorem Proving in Lean 4 | Lean | 289 |
| 231,826 | Lean | 247 | |
| 271,442 | Functional Programming in Lean | Lean | 204 |
| 306,858 | Document Generator for Lean 4 | Lean | 176 |
| 354,240 | An external lean checker with a proof of consistency | Lean | 148 |
| 379,551 | The Lean reference manual | Lean | 136 |
| 398,359 | Lean theorem prover version 0.2 (it supports standard and HoTT modes) | C++ | 128 |
| 406,108 | A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments. | Lean | 125 |
| 416,688 | Armv8 Native Code Symbolic Simulator in Lean | Lean | 121 |
| 436,786 | Extension for VS Code that provides support for the older Lean 3 language. Succeeded by vscode-lean4 ('lean4' in the extensions menu) for the Lean 4 language. | TypeScript | 114 |
| 452,649 | SampCert : Verified Differential Privacy | Lean | 109 |
| 480,756 | **(Deprecated: Merged into Lean 4)** Lean 4 build system and package manager with configuration files written in Lean. | Lean | 101 |
| 499,807 | CMU Undergrad Course | TeX | 96 |
| 550,027 | (Mirror) A Machine-to-Machine Interaction System for Lean 4 | Lean | 85 |
| 566,039 | Skills for AIs using the Lean programming language and theorem prover — proofs, toolchain setup, bisection, and more | Shell | 82 |
| 655,623 | Emacs mode for Lean | Emacs Lisp | 68 |
| 663,577 | LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4. | Lean | 67 |
| 687,767 | Reference type checker for the Lean theorem prover | Haskell | 64 |
| 723,106 | Lean | 60 | |
| 752,777 | This package provides an interface and foundation for verified SAT reasoning | Lean | 57 |
| 785,713 | SQLite bindings for Lean | C | 54 |
| 797,173 | Package registry for Lean/Lake. | Vue | 53 |
| 797,173 | A formalization of ML kernel languages | C | 53 |
| 834,115 | GitHub action for standard CI in Lean projects | Shell | 50 |
| 834,115 | A verified tensor library in Lean | Lean | 50 |
Among 94,827 organizations
16k–25k stars: 923 organizations, including leanprover
Stars along the bottom, and organizations in each band on a log scale
Where the stars are
Languages
- Lean 13.1k stars, 73% · 18 repos
- C++ 2.3k stars, 13% · 2 repos
- Rust 678 stars, 4% · 1 repo
- TypeScript 431 stars, 2% · 2 repos
- Shell 132 stars, 1% · 2 repos
- C 107 stars, 1% · 2 repos
- TeX 96 stars, 1% · 1 repo
- Emacs Lisp 68 stars, <1% · 1 repo
and 2 more languages
When they were made
31 repos with 50+ stars, made between 2013 and 2026
Quick stats
- Next rank
- +1 star to reach #2,085
- Next milestone
- +16,940 stars to reach the top 1%
- Public repos
- 213, 31 with 50+ stars
- Popular repos
- 18 over 100 stars, 2 over 1k stars
- Top repo
- lean4, #5,787 of all repos, 55% of stars
- Smaller repos
- 1,025 stars from repos under 50