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 fada3e8 builds on the recent leanprover/lean4:v4.13.0-rc3
mathlib
The math library of Lean 4
Commit 880f820 builds on the old leanprover/lean4:v4.11.0
LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Commit 21f7dea builds on the recent leanprover/lean4:v4.13.0-rc3
paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
Commit 145ab7f builds on the old leanprover/lean4:v4.11.0-rc2
scilean
Scientific computing in Lean 4
Commit ad3ba5f builds on the recent leanprover/lean4:v4.13.0-rc3
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit dd04633 builds on the recent leanprover/lean4:v4.13.0-rc3
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit a7fefe8 builds on the old leanprover/lean4:v4.7.0
lean4-metaprogramming-book
Commit b20a886 builds on the recent leanprover/lean4:v4.13.0-rc3
aesop
White-box automation for Lean 4
Commit 7789eca builds on the recent leanprover/lean4:v4.13.0-rc3
equational_theories
A project to map out the relations between different equational theories of Magmas.
Commit 80f5638 builds on the recent leanprover/lean4:v4.13.0-rc3
ntptutorial
Tutorial on neural theorem proving
Newly Created Commit 36cf0d0 builds on the recent leanprover/lean4:v4.13.0-rc3
LeanSudoku
Playing Sudoku in the Lean 4 proof assistant
Commit 65faab7 builds on the recent leanprover/lean4:v4.13.0-rc3
ExFormMathL4
Commit 39a5192 builds on the recent leanprover/lean4:v4.13.0-rc3
LeanCourse
Bonn Lean course for winter 24/25
Commit 7789eca builds on the recent leanprover/lean4:v4.13.0-rc3
equational_theories
A project to map out the relations between different equational theories of Magmas.
Commit d1d3854 builds on the recent leanprover/lean4:v4.13.0-rc3
TensorLib
A verified tensor library in Lean
Commit e9e1de6 builds on the recent leanprover/lean4:v4.13.0-rc3
NewProject
Commit 16cd688 builds on the recent leanprover/lean4:v4.13.0-rc3
CommComp
Formalization of communication complexity in Lean
Commit 95d4f48 fails to build on leanprover/lean4:v4.13.0-rc3
rubik
Lean 4 formalization of Rubik's cubes
Commit 1020b88 builds on the recent leanprover/lean4:v4.13.0-rc3
MetaExamples
Examples using MetaProgramming for writing tactics etc.
Commit a8e927a builds on the old leanprover/lean4:v4.11.0-rc2
tutorial
Aeneas tutorial for ICFP
Recently Updated Commit fada3e8 builds on the recent leanprover/lean4:v4.13.0-rc3
mathlib
The math library of Lean 4
Commit 7f0d4a0 builds on the recent leanprover/lean4:v4.13.0-rc3
EulerProducts
An attempt at formalizing facts on Euler products in Lean
Commit 3518550 builds on the recent leanprover/lean4:v4.13.0-rc3
testing_lower_bounds
Information theory and hypothesis testing, in Lean
Commit c0fe06c builds on the recent leanprover/lean4:v4.13.0-rc3
maze
maze game encoded in Lean 4 syntax
Commit 39a5192 builds on the recent leanprover/lean4:v4.13.0-rc3
LeanCourse
Bonn Lean course for winter 24/25
Commit 202c52e builds on the recent leanprover/lean4:v4.13.0-rc3
SSA
A minimal development of SSA theory
Commit c783b7a builds on the recent leanprover/lean4:v4.13.0-rc3
hep_lean
A project to digitalise results from high energy physics into Lean.
Commit a4a366d builds on the recent leanprover/lean4:v4.13.0-rc1
carleson
A formalized proof of Carleson's theorem in Lean
Commit 364815b builds on the recent leanprover/lean4:v4.13.0-rc3
Zklib
A Library for Formally Verified Cryptographic Proof Systems
Commit 5b8d60c builds on the recent leanprover/lean4:v4.13.0-rc3
egg
A (WIP) equality saturation tactic for Lean based on egg.