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 bc87839 builds on the recent leanprover/lean4:v4.13.0-rc3
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 c3c14d4 builds on the recent leanprover/lean4:v4.13.0-rc3
paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
Commit 145ab7f builds on the old leanprover/lean4:v4.11.0-rc2
scilean
Scientific computing in Lean 4
Commit daf1ed9 builds on the recent leanprover/lean4:v4.13.0-rc3
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit 7246ae1 builds on the old leanprover/lean4:v4.7.0
lean4-metaprogramming-book
Commit 3ab2c72 builds on the recent leanprover/lean4:v4.13.0-rc1
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit b20a886 builds on the recent leanprover/lean4:v4.13.0-rc3
aesop
White-box automation for Lean 4
Commit 80f5638 builds on the recent leanprover/lean4:v4.13.0-rc3
ntptutorial
Tutorial on neural theorem proving
Commit 1aca48a builds on the recent leanprover/lean4:v4.13.0-rc1
PFR
Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)
Newly Created Commit b73afda builds on the recent leanprover/lean4:v4.13.0-rc3
ExFormMathL4
Commit e7b028a builds on the recent leanprover/lean4:v4.13.0-rc3
equational_theories
A project to map out the relations between different equational theories of Magmas.
Commit d1d3854 builds on the recent leanprover/lean4:v4.13.0-rc3
TensorLib
A verified tensor library in Lean
Commit e9e1de6 builds on the recent leanprover/lean4:v4.13.0-rc3
NewProject
Commit 16cd688 builds on the recent leanprover/lean4:v4.13.0-rc3
CommComp
Formalization of communication complexity in Lean
Commit 95d4f48 fails to build on leanprover/lean4:v4.13.0-rc3
rubik
Lean 4 formalization of Rubik's cubes
Commit 1020b88 builds on the recent leanprover/lean4:v4.13.0-rc3
MetaExamples
Examples using MetaProgramming for writing tactics etc.
Commit a8e927a builds on the old leanprover/lean4:v4.11.0-rc2
tutorial
Aeneas tutorial for ICFP
Commit 3d6d72f builds on the recent leanprover/lean4:v4.13.0-rc3
sadol
Symbolic and Automatic Differentiation of Languages in Lean
Commit 3ec2fa0 builds on the recent leanprover/lean4:v4.13.0-rc3
Calculemus2_es
Ejercicios de demostración con Lean4 e Isabelle/HOL.
Recently Updated Commit e7b028a builds on the recent leanprover/lean4:v4.13.0-rc3
equational_theories
A project to map out the relations between different equational theories of Magmas.
Commit 4ae310f builds on the recent leanprover/lean4:v4.13.0-rc3
Project
Template for blueprint-driven formalization projects in Lean.
Commit 91eb658 builds on the recent leanprover/lean4:v4.13.0-rc3
InfinityCosmos
A blueprint for a formalization of infinity-cosmos theory in Lean.
Commit bc87839 builds on the recent leanprover/lean4:v4.13.0-rc3
mathlib
The math library of Lean 4
Commit 3679aba builds on the recent leanprover/lean4:v4.13.0-rc3
expdb
Exponent pair database
Commit 0ad8dee builds on the recent leanprover/lean4:v4.13.0-rc3
smt
Tactics for discharging Lean goals into SMT solvers.
Commit d2e847c builds on the recent leanprover/lean4:v4.13.0-rc3
miniF2F-lean4
miniF2F dataset ported into Lean 4
Commit 31d09b1 builds on the recent leanprover/lean4:v4.13.0-rc1
FormalBook
Formalizing "Proofs from THE BOOK"
Commit c3c14d4 builds on the recent leanprover/lean4:v4.13.0-rc3
paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
Commit 1aca48a builds on the recent leanprover/lean4:v4.13.0-rc1
PFR
Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)