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 cc49526 builds on the recent leanprover/lean4:v4.10.0-rc2
mathlib
The math library of Lean 4
Commit 91dbe27 builds on the recent leanprover/lean4:v4.10.0-rc2
LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Commit f53f5a5 builds on the recent leanprover/lean4:v4.10.0-rc2
examples
Lean theorem proving interface which feels like pen-and-paper proofs.
Commit ab76968 builds on the recent leanprover/lean4:v4.9.1
scilean
Scientific computing in Lean 4
Commit d2b1546 builds on the recent leanprover/lean4:v4.10.0-rc2
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit 4ffaf96 builds on the old leanprover/lean4:v4.7.0
lean4-metaprogramming-book
Commit 622d52c builds on the recent leanprover/lean4:v4.10.0-rc2
aesop
White-box automation for Lean 4
Commit fae4ceb builds on the recent leanprover/lean4:v4.10.0-rc2
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit 80f5638 builds on the recent leanprover/lean4:v4.10.0-rc2 after lake update
ntptutorial
Tutorial on neural theorem proving
Commit 44ddc83 builds on the old leanprover/lean4:v4.8.0
PrimeNumberTheoremAnd
blueprint for prime number theorem and more
Newly Created Commit 2a6f787 builds on the recent leanprover/lean4:v4.10.0-rc2
rust-lean-models
Lean models of Rust libraries
Commit b424b1c builds on the recent leanprover/lean4:v4.10.0-rc2 after lake update
evmyul
Executable formal model of the EVM and Yul in Lean 4.
Commit 5e45c1b fails to build on leanprover/lean4:v4.10.0-rc2
HadwigerNelson
Hadwiger-Nelson Problem Formalization in Lean 4
Commit ff7808b fails to build on leanprover/lean4:v4.10.0-rc2
lffi
Commit 2ca670d builds on the old leanprover/lean4:v4.7.0
Game
Commit 64d3e1f builds on the recent leanprover/lean4:v4.10.0-rc2
jixia
A static analysis tool for Lean 4.
Commit f1912c3 builds on the old leanprover/lean4:v4.8.0
lib
LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.
Commit 0be7902 builds on the old leanprover/lean4:v4.8.0
ray
Conservative floating point interval arithmetic in Lean
Commit dbca34c builds on the recent leanprover/lean4:v4.10.0-rc2
DGAlgorithms
Distributed Graph Algorithms in Lean
Commit ac65108 builds on the recent leanprover/lean4:v4.10.0-rc2
Koch
Koch 2D snowflake generator for 4D Golf
Recently Updated Commit 2800f1a builds on the old leanprover/lean4:v4.8.0-rc1 after lake update
llmlean
LLMs + Lean, on your laptop or in the cloud
Commit b424b1c builds on the recent leanprover/lean4:v4.10.0-rc2 after lake update
evmyul
Executable formal model of the EVM and Yul in Lean 4.
Commit eb4d25a builds on the recent leanprover/lean4:v4.10.0-rc2
sampcert
SampCert : Verified Differential Privacy
Commit 07da422 builds on the old leanprover/lean4:v4.5.0
formalising-mathematics-2024
Formalising Mathematics; a course for undergraduate mathematicians. Ran between January and March 2024.
Commit 96dd869 builds on the recent leanprover/lean4:v4.10.0-rc2
lean99
These are Lean translations of Ninety-Nine Haskell Problems (WIP)
Commit cc49526 builds on the recent leanprover/lean4:v4.10.0-rc2
mathlib
The math library of Lean 4
Commit 1c0f127 builds on the recent leanprover/lean4:v4.10.0-rc2
Lean Book
mdbook template for lean project
Commit b25347b builds on the recent leanprover/lean4:v4.10.0-rc2
compfiles
Catalog Of Math Problems Formalized In Lean
Commit 2c6d8f6 builds on the recent leanprover/lean4:v4.10.0-rc2 after lake update
pdl
Commit f1912c3 builds on the old leanprover/lean4:v4.8.0
lib
LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.