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 9a3c534 builds on the recent leanprover/lean4:v4.18.0-rc1
mathlib
The math library of Lean 4
Commit e2aebda builds on the recent leanprover/lean4:v4.18.0-rc1
LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Commit 1020766 builds on the recent leanprover/lean4:v4.17.0
paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
Commit 47d204c builds on the recent leanprover/lean4:v4.17.0
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit 53f112d builds on the old leanprover/lean4:v4.15.0
scilean
Scientific computing in Lean 4
Commit 2bb49af 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 b8e1430 builds on the recent leanprover/lean4:v4.18.0-rc1
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit ec060e0 builds on the recent leanprover/lean4:v4.18.0-rc1
aesop
White-box automation for Lean 4
Commit 731400d builds on the recent leanprover/lean4:v4.17.0
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 c2639ea builds on the recent leanprover/lean4:v4.18.0-rc1
combinatorial-games
Combinatorial game library in Lean 4
Commit df5700e fails to build on leanprover/lean4:v4.17.0
lean4-analysis-tao
Formalization of "Analysis I" by Terence Tao
Commit ecdde79 builds on the recent leanprover/lean4:v4.17.0
LeanBanachTarski
Commit be838b2 builds on the recent leanprover/lean4:v4.17.0
Toric
Formalisation of toric varieties in Lean 4
Commit 34dd41b builds on the recent leanprover/lean4:v4.17.0
veil
A verifier for automated and interactive proofs about transition systems. This repository is a public mirror with stable development snapshots. Submit issues and PRs here.
Commit 55ae927 builds on the recent leanprover/lean4:v4.18.0-rc1
algebra
Algebra library for Lean 4
Commit bf077ed builds on the recent leanprover/lean4:v4.17.0
VD
Formalizing Value Distribution Theory
Commit dab9d9c builds on the recent leanprover/lean4:v4.17.0
PfsProgs25
Code for the course "Proofs and Programs", January 2025, IISc
Commit 415892f builds on the old 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 ff43ad7 builds on the recent leanprover/lean4:v4.17.0-rc1
Zklib
Formally Verified SNARKs in Lean
Recently Updated Commit 9a3c534 builds on the recent leanprover/lean4:v4.18.0-rc1
mathlib
The math library of Lean 4
Commit aa47907 builds on the recent leanprover/lean4:v4.18.0-rc1
compfiles
Catalog Of Math Problems Formalized In Lean
Commit 0834506 builds on the old leanprover/lean4:v4.3.0
math2001
Commit b8e1430 builds on the recent leanprover/lean4:v4.18.0-rc1
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit 53f112d builds on the old leanprover/lean4:v4.15.0
scilean
Scientific computing in Lean 4
Commit 5dce4bc builds on the recent leanprover/lean4:v4.17.0-rc1
foundation
Formalization of Mathematical Logic
Commit f27b41a builds on the old leanprover/lean4:v4.7.0
Game
Knights and Knaves Educational Game in Lean 4
Commit 834277b builds on the recent leanprover/lean4:v4.18.0-rc1
lean-machines
a Lean4 framework for the modeling and refinement of stateful systems
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 78c191d builds on the recent leanprover/lean4:v4.17.0
LeanAPAP
Formalisation of the Kelley-Meka bound on Roth numbers