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 1fef59c builds on the recent leanprover/lean4:v4.14.0-rc1
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 38f7775 builds on the recent leanprover/lean4:v4.13.0
paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
Commit 7cbec80 builds on the recent leanprover/lean4:v4.13.0
scilean
Scientific computing in Lean 4
Commit 76e9ebe builds on the recent leanprover/lean4:v4.14.0-rc1
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit 1a17cd1 builds on the recent leanprover/lean4:v4.14.0-rc1
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 0f3edc3 builds on the recent leanprover/lean4:v4.13.0
equational_theories
A project to map out the relations between different equational theories of Magmas.
Commit 93bcfd7 builds on the recent leanprover/lean4:v4.14.0-rc1
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 256986c builds on the recent leanprover/lean4:v4.13.0
borel_det
Commit 42dc02b builds on the recent leanprover/lean4:v4.14.0-rc1
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 0c8aa3d builds on the recent leanprover/lean4:v4.13.0
Seymour
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
Recently Updated Commit 0f3edc3 builds on the recent leanprover/lean4:v4.13.0
equational_theories
A project to map out the relations between different equational theories of Magmas.
Commit 1fef59c builds on the recent leanprover/lean4:v4.14.0-rc1
mathlib
The math library of Lean 4
Commit 93bcfd7 builds on the recent leanprover/lean4:v4.14.0-rc1
aesop
White-box automation for Lean 4
Commit 46fb498 builds on the recent leanprover/lean4:v4.13.0
remco-mul
Commit bcad3ee builds on the old leanprover/lean4:v4.11.0
lost-pop-lean
POP Memory Model in Lean
Commit 3b8f5f1 builds on the recent leanprover/lean4:v4.13.0-rc3
lnsym
Armv8 Native Code Symbolic Simulator in Lean
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 76e9ebe builds on the recent leanprover/lean4:v4.14.0-rc1
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit 0f09ff1 builds on the recent leanprover/lean4:v4.13.0-rc3
testing_lower_bounds
Information theory and hypothesis testing, in Lean
Commit d1d3854 builds on the recent leanprover/lean4:v4.13.0
TensorLib
A verified tensor library in Lean