Reservoir indexes, builds, and tests packages within the Lean and Lake ecosystem. If you wish to see your package here, ensure that it meets the Reservoir inclusion criteria .
Most Popular Commit 3368abb builds on the recent leanprover/lean4:v4.16.0-rc2
mathlib
The math library of Lean 4
Commit 2cefd43 builds on the recent leanprover/lean4:v4.16.0-rc2
LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Commit fff3e75 builds on the recent leanprover/lean4:v4.16.0-rc2
paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
Commit 53f112d builds on the recent leanprover/lean4:v4.15.0
scilean
Scientific computing in Lean 4
Commit d78a329 builds on the recent leanprover/lean4:v4.16.0-rc2
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit a2369f6 builds on the old leanprover/lean4:v4.14.0-rc3
equational_theories
A project to map out the relations between different equational theories of Magmas.
Commit 5b23a12 builds on the recent leanprover/lean4:v4.16.0-rc2
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit 7d9e59f builds on the recent leanprover/lean4:v4.16.0-rc2
lean4-metaprogramming-book
Commit caa2968 builds on the recent leanprover/lean4:v4.16.0-rc2
aesop
White-box automation for Lean 4
Commit 80f5638 builds on the recent leanprover/lean4:v4.16.0-rc2
ntptutorial
Tutorial on neural theorem proving
Newly Created Commit 8e3bc47 builds on the recent leanprover/lean4:v4.16.0-rc2
algebra
Algebra library for Lean 4
Commit 415892f builds on the recent leanprover/lean4:v4.15.0-rc1
vqc_in_lean
Lean 4 port of the Verified Quantum Computing. Developed as a personal learning project to deepen understanding of quantum computing concepts and formal verification.
Commit 8937ae0 builds on the recent leanprover/lean4:v4.15.0
leanblas
Bindings and specification for BLAS
Commit 0976f6a builds on the recent leanprover/lean4:v4.16.0-rc2
NodeGraph
Commit 7162921 builds on the recent leanprover/lean4:v4.16.0-rc2
special-numbers
Special Numbers (Chapter 6 from Knuth's Concrete Mathematics)
Commit c673cd6 builds on the old leanprover/lean4:v4.14.0-rc2
FactorizationSystems
Commit 9034b20 builds on the recent leanprover/lean4:v4.15.0
partial-combinatory-algebras
A Lean 4 formalization of partial combinatory algebras.
Commit 2470c19 builds on the recent leanprover/lean4:v4.16.0-rc2
CodeProofTheArena
Lean coding problem solving challenge website with proof verification
Commit 9f3241a builds on the recent leanprover/lean4:v4.15.0-rc1
remco-mul
Commit 9a814a2 builds on the recent leanprover/lean4:v4.16.0-rc2
order-p-q
Lean formalisation of the classification of the groups of order `p * q` where `p` and `q` are prime numbers.
Recently Updated Commit ad2220e builds on the recent leanprover/lean4:v4.16.0-rc2
SSA
A minimal development of SSA theory
Commit 3368abb builds on the recent leanprover/lean4:v4.16.0-rc2
mathlib
The math library of Lean 4
Commit 40eb793 builds on the recent leanprover/lean4:v4.16.0-rc2
lean-machines
a Lean4 framework for the modeling and refinement of stateful systems
Commit 4d43698 builds on the recent leanprover/lean4:v4.15.0
HepLean
A project to digitalise results from high energy physics into Lean.
Commit ec5180c builds on the recent leanprover/lean4:v4.15.0
certifyingDatalog
A certified checker for Datalog entailments, written in Lean
Commit 0138d63 builds on the recent leanprover/lean4:v4.16.0-rc2
carleson
A formalized proof of Carleson's theorem in Lean
Commit 56cbdfe builds on the old leanprover/lean4:v4.12.0-rc1
Clean
Lean circuit DSL for AIR
Commit a8fec24 builds on the recent leanprover/lean4:v4.16.0-rc2
egg
A (WIP) equality saturation tactic for Lean based on egg.
Commit ee110ec builds on the recent leanprover/lean4:v4.16.0-rc2
proofwidgets
Helper toolkit for creating your own Lean 4 UserWidgets
Commit 2f6d2ac fails to build on leanprover/lean4:v4.16.0-rc2
Postgres