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 9da3d90 builds on the recent leanprover/lean4:v4.19.0-rc3
mathlib
The math library of Lean 4
Commit 9498454 builds on the recent leanprover/lean4:v4.18.0
LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Commit 0fb99d8 builds on the recent leanprover/lean4:v4.19.0-rc3
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit 2c9cad0 builds on the recent leanprover/lean4:v4.19.0-rc3
paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
Commit 53f112d builds on the old leanprover/lean4:v4.15.0
scilean
Scientific computing in Lean 4
Commit bc6dc1e 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 f523fcb builds on the recent leanprover/lean4:v4.19.0-rc3
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit 323e9f0 builds on the recent leanprover/lean4:v4.19.0-rc3
aesop
White-box automation for Lean 4
Commit 731400d builds on the recent leanprover/lean4:v4.19.0-rc3
lean4-metaprogramming-book
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.
Newly Created Commit 078a0db builds on the recent leanprover/lean4:v4.19.0-rc3
kimina
A Lean tactic that invokes the Kimina Prover Preview model to offer proof suggestions.
Commit 3118411 builds on the recent leanprover/lean4:v4.19.0-rc3
cryptolib
Commit 02f8d14 builds on the recent leanprover/lean4:v4.18.0-rc1
LeanTeX_Mathlib
LeanTeX pretty printers for mathlib
Commit 6e27ac1 builds on the recent leanprover/lean4:v4.18.0-rc1
NeuralNetworks
Formalization of Neural Networks in Lean 4
Commit c4586f5 builds on the recent leanprover/lean4:v4.18.0-rc1
combinatorial-games
Combinatorial game library in Lean 4
Commit 0be2cbd fails to build on leanprover/lean4:v4.19.0-rc3
lean4-analysis-tao
Formalization of "Analysis I" by Terence Tao
Commit 75d0dab fails to build on leanprover/lean4:v4.19.0-rc3
sqlite
Sqlite3 bindings for lean4
Commit ecdde79 builds on the recent leanprover/lean4:v4.18.0-rc1
LeanBanachTarski
Commit c4f495b builds on the recent leanprover/lean4:v4.19.0-rc3
Toric
Formalisation of toric varieties in Lean 4
Commit 7fd55ea fails to build on leanprover/lean4:v4.18.0
formalising-mathematics
Course on theorem proving with Lean
Recently Updated Commit 750cc34 fails to build on leanprover/lean4:v4.19.0-rc3
LeanLJ
Lennard Jones in Lean
Commit 9da3d90 builds on the recent leanprover/lean4:v4.19.0-rc3
mathlib
The math library of Lean 4
Commit 7ce8ddd builds on the recent leanprover/lean4:v4.18.0
KLR
A formalization of ML kernel languages
Commit a186683 builds on the recent leanprover/lean4:v4.18.0
VCVio
Formalized Cryptography Proofs in Lean 4
Commit c4f495b builds on the recent leanprover/lean4:v4.19.0-rc3
Toric
Formalisation of toric varieties in Lean 4
Commit 9498454 builds on the recent leanprover/lean4:v4.18.0
LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Commit 236d583 builds on the recent leanprover/lean4:v4.18.0-rc1
pdl
Tableaux for Propositional Dynamic Logic in Lean 4 (WORK IN PROGRESS)
Commit 991d95d builds on the recent leanprover/lean4:v4.18.0
Zklib
Formally Verified SNARKs in Lean
Commit 8582a62 builds on the recent leanprover/lean4:v4.19.0-rc3
carleson
A formalized proof of Carleson's theorem in Lean
Commit 9cfd9cd builds on the recent leanprover/lean4:v4.19.0-rc3
Matroid