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 090e243 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 992c4c8 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 c521f01 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 77e137d 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 88f806c 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 a9062de builds on the recent leanprover/lean4:v4.13.0-rc3
LeanCourse
Bonn Lean course for winter 24/25
Commit 88f806c 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 adcdd8b builds on the recent leanprover/lean4:v4.13.0-rc3
compfiles
Catalog Of Math Problems Formalized In Lean
Commit 090e243 builds on the recent leanprover/lean4:v4.13.0-rc3
mathlib
The math library of Lean 4
Commit b424b1c builds on the old leanprover/lean4:v4.10.0 after lake update
evmyul
Executable formal model of the EVM and Yul in Lean 4.
Commit 325da40 builds on the old leanprover/lean4:v4.9.0-rc3
lean-training-data
Commit f959e28 builds on the recent leanprover/lean4:v4.13.0-rc3
GroundZero
Ground Zero: Lean 4 HoTT Library
Commit 32ec426 builds on the recent leanprover/lean4:v4.13.0-rc3
LeanAPAP
Formalisation of the Kelley-Meka bound on Roth numbers
Commit c521f01 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 283abe4 builds on the recent leanprover/lean4:v4.13.0-rc3
testing_lower_bounds
Information theory and hypothesis testing, in Lean
Commit 9362871 builds on the recent leanprover/lean4:v4.13.0-rc3
jixia
A static analysis tool for Lean 4.
Commit 942f45d builds on the recent leanprover/lean4:v4.13.0-rc3
BET
Project for "Machine-Checked Mathematics" at the Lorentz Center