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 c46b5e4 builds on the recent leanprover/lean4:v4.13.0
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
paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
Commit 3df3ceb builds on the recent leanprover/lean4:v4.13.0
scilean
Scientific computing in Lean 4
Commit 31a10a3 builds on the recent leanprover/lean4:v4.13.0
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit 17ea847 builds on the recent leanprover/lean4:v4.13.0
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 8ddda84 builds on the recent leanprover/lean4:v4.13.0-rc4
equational_theories
A project to map out the relations between different equational theories of Magmas.
Commit 5f93489 builds on the recent leanprover/lean4:v4.13.0
aesop
White-box automation for Lean 4
Commit 80f5638 builds on the recent leanprover/lean4:v4.13.0
ntptutorial
Tutorial on neural theorem proving
Newly Created Commit 46fb498 builds on the recent leanprover/lean4:v4.13.0
remco-mul
Commit 7173622 builds on the recent leanprover/lean4:v4.13.0
order-pq
Lean formalisation of the classification of the groups of order `p * q` where `p` and `q` are prime numbers.
Commit 83e4f2e fails to build on leanprover/lean4:v4.13.0
borel_det
Commit d212dd7 builds on the recent leanprover/lean4:v4.13.0
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.13.0
LeanSudoku
Playing Sudoku in the Lean 4 proof assistant
Commit 42a29f0 builds on the recent leanprover/lean4:v4.13.0
ExFormMathL4
Commit c318c9f builds on the recent leanprover/lean4:v4.13.0
LeanCourse
Bonn Lean course for winter 24/25
Commit 8ddda84 builds on the recent leanprover/lean4:v4.13.0-rc4
equational_theories
A project to map out the relations between different equational theories of Magmas.
Recently Updated Commit c46b5e4 builds on the recent leanprover/lean4:v4.13.0
mathlib
The math library of Lean 4
Commit 8ddda84 builds on the recent leanprover/lean4:v4.13.0-rc4
equational_theories
A project to map out the relations between different equational theories of Magmas.
Commit 0f09ff1 builds on the recent leanprover/lean4:v4.13.0-rc3
testing_lower_bounds
Information theory and hypothesis testing, in Lean
Commit 15b5ff3 builds on the recent leanprover/lean4:v4.13.0
UnicodeBasic
Basic Unicode support for Lean 4
Commit f3be290 builds on the recent leanprover/lean4:v4.13.0
SSA
A minimal development of SSA theory
Commit a2b708e builds on the recent leanprover/lean4:v4.13.0-rc1
ConNF
A formal consistency proof of Quine's set theory New Foundations
Commit 1f1b175 builds on the recent leanprover/lean4:v4.13.0-rc4
foundation
Lean4 Logic Formalization
Commit 3d85ae5 builds on the recent leanprover/lean4:v4.13.0
Calculemus2
Proof exercises in Lean4 and Isabelle/HOL
Commit 77448d6 builds on the recent leanprover/lean4:v4.13.0
llmlean
LLMs + Lean, on your laptop or in the cloud
Commit 0664171 builds on the recent leanprover/lean4:v4.13.0
Calculemus2_es
Ejercicios de demostración con Lean4 e Isabelle/HOL.