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
haruhisa-enomoto/mathlib4-all-tactics
Markdown file of the list and explanations of all mathlib4 tactics
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
Timeroot/computableReal
computable implementation of real numbers in Lean4
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
alexkeizer/qpf
A WIP definitional (co)datatype package for Lean4
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
input-output-hk/Blaster
SMT-based reasoning core for Lean4
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
joehendrix/lean-crypto
Cryptographic routines for the Lean 4 language
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
leanprover/KLR
A formalization of ML kernel languages
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
reilabs/proven-zk
A support library for working with zero knowledge cryptography in Lean 4.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
Verified-zkEVM/EvmAsm
No package description is available.
Reservoir metadata only · declarations not indexed
leanprover/leansqlite
SQLite bindings for Lean
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
leanprover-community/SphereEversion
Formalization of the existence of sphere eversions
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
argumentcomputer/Wasm.lean
A WebAssembly implementation in Lean4
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
AxiomMath/FelConjecture
Lean formalizations for the paper "Fel's conjecture on syzigies of numerical semigroups"
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.