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
siddhartha-gadgil/MetaExamples
Examples using MetaProgramming for writing tactics etc.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
Trequetrum/Game
Make/Encode some basic logic puzzles
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
codyroux/traat
Lean formalization of selected lemmas from "Term Rewriting and All That"
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
dwrensha/rupert
Formalization of the Rupert Problem for convex polyhedra.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
fpvandoorn/LeanCourse25
No package description is available.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
katydid/regexderiv
Proofs written in Lean4 for the core katydid validation algorithm
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
nomeata/wfinduct
No package description is available.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
adomani/mA4N1
MA4N1 Theorem Proving with Lean
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
argumentcomputer/RustFFI.lean
Template for Lean<->Rust FFI
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
Beneficial-AI-Foundation/FloatSpec
Formally Verified Float Implementation with lean4
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
digama0/ast_export
AST export from Lean 4
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
draperlaboratory/ELFSage
A toy ELF parser/validator
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.