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 624b492 builds on the recent leanprover/lean4:v4.11.0-rc3
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.11.0
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 a7fd140 builds on the recent leanprover/lean4:v4.11.0-rc3
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 6c89b67 builds on the recent leanprover/lean4:v4.11.0-rc3
aesop
White-box automation for Lean 4
Commit 80f5638 builds on the recent leanprover/lean4:v4.11.0 after lake update
ntptutorial
Tutorial on neural theorem proving
Commit 44d77ec builds on the recent leanprover/lean4:v4.11.0-rc2
PFR
Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)
Newly Created Build data not currently included on Reservoir. See the package repository's CI instead.
tutorial
Aeneas tutorial for ICFP
Commit d39896e builds on the recent leanprover/lean4:v4.11.0
SHerLOC
A verified StableHLO in Lean
Commit 70ae488 builds on the recent leanprover/lean4:v4.11.0 after lake update
Project
Structure in Prime Gaps - Formalized
Commit 4e0b86a builds on the recent leanprover/lean4:v4.11.0 after lake update
lean-machines-examples
Example specifications for the Lean Machines modelling framework
Commit e739cdb builds on the recent leanprover/lean4:v4.11.0 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.11.0
expdb
Exponent pair database
Commit 6fe1fcd builds on the recent leanprover/lean4:v4.11.0-rc3
chromatic_polynomial
Chromatic polynomial in Lean4
Commit 624837e builds on the recent leanprover/lean4:v4.11.0 after lake update
InfinityCosmos
A blueprint for a formalization of infinity-cosmos theory in Lean.
Commit 17cb327 fails to build on leanprover/lean4:v4.11.0-rc3
lean-raylib
Lean4 bindings for raylib
Commit 868cf62 fails to build on leanprover/lean4:v4.11.0
UnicodeSkipListTableExample
A library that shows how to use the Unicode skip list tables generation tool to create a table to test if a codepoint is numeric.
Recently Updated Commit 624b492 builds on the recent leanprover/lean4:v4.11.0-rc3
mathlib
The math library of Lean 4
Commit 41fccc3 builds on the recent leanprover/lean4:v4.11.0
duality
Duality theory in linear optimization and its extensions
Commit 6bcf0b4 builds on the old leanprover/lean4:v4.10.0
miniF2F-lean4
Commit 601dc5f builds on the recent leanprover/lean4:v4.11.0
pdl
Commit a7fd140 builds on the recent leanprover/lean4:v4.11.0-rc3
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit 469f522 builds on the recent leanprover/lean4:v4.11.0 after lake update
compfiles
Catalog Of Math Problems Formalized In Lean
Commit 5cdc785 builds on the recent leanprover/lean4:v4.11.0 after lake update
Lean by Example
コード例で学ぶ Lean 言語
Commit 625021a builds on the recent leanprover/lean4:v4.11.0 after lake update
Calculemus2
Proof exercises in Lean4 and Isabelle/HOL
Commit 139af3f builds on the recent leanprover/lean4:v4.11.0 after lake update
leancolls
WIP collections library for Lean 4
Commit 2a65e91 builds on the recent leanprover/lean4:v4.11.0 after lake update
flt-regular
Fermat's Last Theorem for regular primes