Pinned Reservoir catalog
Search package metadata by name, description, keyword, license, toolchain, or dependency name. Proof-indexed projects connect to their exact Therefore declaration records.
782 packages
782 packages pinned from Reservoir
raphaelrrcoelho/MathFin
Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
VCA-EPFL/graphiti
Verified graph rewriting (for dataflow circuits).
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
Vilin97/Clawristotle
OpenClaw-style theorem proving
Reservoir metadata only · declarations not indexed
abdoo8080/cvc5
A Foreign Function Interface (FFI) to cvc5 solver in Lean.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
alexjbest/leaff
Leaff is a diff tool for Lean environments
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
mortarsanjaya/IMOSLLean4
Formalization of IMO shortlist problems in Lean 4
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
paulch42/leanSpec
Program Specification in Lean 4
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
pitmonticone/ItaLean
Repository hosting the resources for the conference "ItaLean 2025", held in Bologna, Italy, December 9–12, 2025.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
Seasawher/mdgen
Tool to generate markdown files from lean files.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
vltanh/lean4-analysis-tao
Formalization of "Analysis I" by Terence Tao
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
Anderssorby/SDL
SDL2 bindings for lean
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
brettkoonce/lean4-mlir
Lean specification of neural architectures with verified IREE codegen.
Reservoir metadata only · declarations not indexed