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
verified-optimization/CvxLean
Convex optimization modeling in Lean 4
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
SrGaabriel/soma-workspace
⚗️ | Soma is a general-purpose dependently-typed functional programming language powered by Interaction Nets with a minimal runtime.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
sunblaze-ucb/verina
Verina (Verifiable Code Generation Arena) is a high-quality benchmark enabling a comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
dwrensha/maze
maze game encoded in Lean 4 syntax
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
starkware-libs/verification
No package description is available.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
midspiral/LemmaScript
verification toolchain for TypeScript (Tech Preview)
Reservoir metadata only · declarations not indexed
Vilin97/lean-pool
No package description is available.
Reservoir metadata only · declarations not indexed
emilyriehl/Game
A game introducing proofs, dependent type theory, and Lean prepared for a first year seminar course at Johns Hopkins in Fall 2025.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
leanprover/leanInk
LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
AlexKontorovich/Game
RealAnalysisGame
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
verse-lab/Velvet
An auto-active verifier embedded into Lean
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
BoltonBailey/FormalSnarksProject
A formal verification of Linear PCP SNARKs.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.