Discover trending Lean
open-source projects

37
88
153
Our great sponsors
  • InfluxDB - Power Real-Time Data Analytics at Scale
  • WorkOS - The modern identity platform for B2B SaaS
  • SaaSHub - Software Alternatives and Reviews
Mentions
@
Stars Project Description
- 3,608 Lean 4 programming language and theorem prover
- 1,619 Lean 3's obsolete mathematical components library: please use mathlib4
- 678 The math library of Lean 4
- 493 Demo for high-performance type theory elaboration
- 322 Simple verification of Rust programs via functional purification in Lean 2(!)
- 290 Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.
- 290 Material for Kevin Buzzard's 2021 TCC courrse on formalising mathematics.
- 193
- 184 Standard Library for Lean 4
- 156 Lean 3 material related to Imperial College's "Introduction to University Mathematics" course
- 152 💧 Liquid Tensor Experiment
- 116 Lean material for Kevin Buzzard's Jan-Mar 2022 course on formalising mathematics.
- 110 A simple raytracer written in Lean 4
- 103 Interactive neural theorem proving in Lean
- 103 A formal proof of the independence of the continuum hypothesis
- 97 Companion files for Logical Verification 2020–2021 at VU Amsterdam
- 76
- 74 A gamification of the theorems in MATH40002 Analysis 1
- 72 HoTT in Lean 3
- 60 Definitional implementation of Cedar language and utilities for DRT

Popular Lean Topics