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
leanprover/sampcert
SampCert : Verified Differential Privacy
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
optsuite/optlib
No package description is available.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
yuma-mizuno/lean-math-workshop
数学系のためのLean勉強会
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
thefundamentaltheor3m/SpherePacking
A Lean formalisation of Maryna Viazovska's Fields Medal-winning solution to the sphere packing problem in dimension 8.
Reservoir metadata only · declarations not indexed
JOSHCLUNE/Hammer
LeanHammer is an automated reasoning tool for Lean that brings together multiple proof search and reconstruction techniques and combines them into one tool.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
Verilean/sparkle
A type-safe, formally verifiable HDL compiler in Lean 4. Inspired by Clash, built for high-assurance hardware synthesis.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
dwrensha/animate
tool for turning Lean proofs into Blender animations
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
NethermindEth/evmyul
Executable formal model of the EVM and Yul in Lean 4.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
mirefek/tactic-programming-beginner-guide
Beginner's guide to Tactic Programming in Lean
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
GasStationManager/LeanTool
A "code intepreter" for Lean
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
marcusrossel/egg
A deprecated equality saturation tactic for Lean based on egg.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
leanprover-community/ConNF
A formal consistency proof of Quine's set theory New Foundations
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.