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 3fecb24 builds on the recent leanprover/lean4:v4.12.0-rc1
mathlib
The math library of Lean 4
Commit 880f820 builds on the recent leanprover/lean4:v4.11.0
LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Commit 5c3f55b builds on the recent leanprover/lean4:v4.12.0-rc1
examples
Lean theorem proving interface which feels like pen-and-paper proofs.
Commit 061b964 builds on the recent leanprover/lean4:v4.11.0-rc2
scilean
Scientific computing in Lean 4
Commit 8feac54 builds on the recent leanprover/lean4:v4.12.0-rc1
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit 4ffaf96 builds on the old leanprover/lean4:v4.7.0
lean4-metaprogramming-book
Commit 7066ad8 builds on the old leanprover/lean4:v4.10.0
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit e291aa4 builds on the recent leanprover/lean4:v4.12.0-rc1
aesop
White-box automation for Lean 4
Commit 80f5638 builds on the recent leanprover/lean4:v4.12.0-rc1 after lake update
ntptutorial
Tutorial on neural theorem proving
Commit 2cd83b1 builds on the recent leanprover/lean4:v4.12.0-rc1
PFR
Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)
Newly Created Commit 9185116 builds on the recent leanprover/lean4:v4.12.0-rc1
MetaExamples
Examples using MetaProgramming for writing tactics etc.
Build data not currently included on Reservoir. See the package repository's CI instead.
tutorial
Aeneas tutorial for ICFP
Build data not currently included on Reservoir. See the package repository's CI instead.
Calculemus2_es
Ejercicios de demostración con Lean4 e Isabelle/HOL.
Commit d39896e builds on the recent leanprover/lean4:v4.12.0-rc1
SHerLOC
A verified StableHLO in Lean
Commit 70ae488 builds on the recent leanprover/lean4:v4.12.0-rc1 after lake update
Project
Structure in Prime Gaps - Formalized
Commit 4e0b86a builds on the recent leanprover/lean4:v4.12.0-rc1 after lake update
lean-machines-examples
Example specifications for the Lean Machines modelling framework
Commit e739cdb builds on the recent leanprover/lean4:v4.12.0-rc1 after lake update
lean-machines
a Lean4 framework for the modeling and refinement of stateful systems
Commit 68e62f8 builds on the recent leanprover/lean4:v4.12.0-rc1
expdb
Exponent pair database
Commit 6fe1fcd builds on the recent leanprover/lean4:v4.11.0-rc3
chromatic_polynomial
Chromatic polynomial in Lean4
Commit ce22c73 builds on the recent leanprover/lean4:v4.12.0-rc1
InfinityCosmos
A blueprint for a formalization of infinity-cosmos theory in Lean.
Recently Updated Commit 8d57ab3 builds on the recent leanprover/lean4:v4.12.0-rc1
testing_lower_bounds
Lower bounds for hypothesis testing and estimation, in Lean
Commit 3fecb24 builds on the recent leanprover/lean4:v4.12.0-rc1
mathlib
The math library of Lean 4
Commit 59b051c builds on the recent leanprover/lean4:v4.12.0-rc1
Regex
Commit 6fbe8c2 builds on the old leanprover/lean4:v4.8.0 after lake update
formal_book
Formalizing "Proofs from THE BOOK"
Commit 1805c5a builds on the recent leanprover/lean4:v4.12.0-rc1 after lake update
arithmetization
Formalization of Arithmetization of Metamathematics
Commit ba5a5fd builds on the recent leanprover/lean4:v4.12.0-rc1
egg
A (WIP) equality saturation tactic for Lean based on egg.
Commit d881aa5 builds on the recent leanprover/lean4:v4.12.0-rc1
compfiles
Catalog Of Math Problems Formalized In Lean
Commit a51b8ed builds on the recent leanprover/lean4:v4.12.0-rc1
Curl
Lean 4 bindings to libcurl
Commit 3331c49 builds on the recent leanprover/lean4:v4.12.0-rc1 after lake update
animate
tool for turning Lean proofs into Blender animations
Commit 17d740e builds on the recent leanprover/lean4:v4.12.0-rc1
mk-exercise
Simple and intuitive tool to manage exercises in textbooks written in Lean.