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 fb23240 builds on the recent leanprover/lean4:v4.14.0-rc2
mathlib
The math library of Lean 4
Commit f6a3f14 builds on the old leanprover/lean4:v4.11.0
LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Commit e2b76ee builds on the recent leanprover/lean4:v4.14.0-rc2
paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
Commit 92b1246 builds on the recent leanprover/lean4:v4.14.0-rc2
scilean
Scientific computing in Lean 4
Commit f56857a builds on the recent leanprover/lean4:v4.14.0-rc2
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit 01f4969 builds on the recent leanprover/lean4:v4.14.0-rc2
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit 3f28838 builds on the old leanprover/lean4:v4.7.0
lean4-metaprogramming-book
Commit 9a7479f builds on the recent leanprover/lean4:v4.14.0-rc2
equational_theories
A project to map out the relations between different equational theories of Magmas.
Commit de91b59 builds on the recent leanprover/lean4:v4.14.0-rc2
aesop
White-box automation for Lean 4
Commit 80f5638 builds on the recent leanprover/lean4:v4.14.0-rc2
ntptutorial
Tutorial on neural theorem proving
Newly Created Commit d7f2512 builds on the recent leanprover/lean4:v4.14.0-rc2
CodeProofTheArena
Lean coding problem solving challenge website with proof verification
Commit 9f3241a builds on the recent leanprover/lean4:v4.14.0-rc2
remco-mul
Commit c90caa1 builds on the recent leanprover/lean4:v4.14.0-rc2
order-pq
Lean formalisation of the classification of the groups of order `p * q` where `p` and `q` are prime numbers.
Commit 256986c builds on the recent leanprover/lean4:v4.13.0
borel_det
Commit 42dc02b builds on the recent leanprover/lean4:v4.14.0-rc2
plausible
Commit 8e24b93 builds on the recent leanprover/lean4:v4.13.0-rc4
FMCn_Lean
Repositório destinado às práticas de Lean4 da Monitoria de FMCn.
Commit 5ae790f builds on the recent leanprover/lean4:v4.13.0-rc4
Seminar
Past contents of Lean Seminars in Bonn
Commit c5d60b8 builds on the recent leanprover/lean4:v4.14.0-rc2
LeanSudoku
Playing Sudoku in the Lean 4 proof assistant
Commit cfdc916 builds on the recent leanprover/lean4:v4.14.0-rc2
Seymour
Commit be2e471 builds on the recent leanprover/lean4:v4.14.0-rc2
ExFormMathL4
Recently Updated Commit fb23240 builds on the recent leanprover/lean4:v4.14.0-rc2
mathlib
The math library of Lean 4
Commit b9fffc6 builds on the recent leanprover/lean4:v4.14.0-rc2
carleson
A formalized proof of Carleson's theorem in Lean
Commit 059eb7e builds on the recent leanprover/lean4:v4.14.0-rc2
doc-gen4
Document Generator for Lean 4
Commit 01f4969 builds on the recent leanprover/lean4:v4.14.0-rc2
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit ec3e131 builds on the old leanprover/lean4:nightly
NKL
A formalization of the NKI ISA
Commit 70a3b6a builds on the recent leanprover/lean4:v4.14.0-rc2
compfiles
Catalog Of Math Problems Formalized In Lean
Commit 9fa4177 builds on the recent leanprover/lean4:v4.14.0-rc2
LeanCourse
Bonn Lean course for winter 24/25
Commit 628c142 fails to build on leanprover/lean4:v4.14.0-rc2
GameTheory
Commit 42dc02b builds on the recent leanprover/lean4:v4.14.0-rc2
plausible
Commit 26bcae6 builds on the recent leanprover/lean4:v4.14.0-rc2
proofwidgets
Helper toolkit for creating your own Lean 4 UserWidgets