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
GasStationManager/SafeVerify
A Lean4 script for robustly verifying submitted proofs of theorems and implementations of functions
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
leanprover-community/mathport
Mathport is a tool for porting Lean3 projects to Lean4
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
Verified-zkEVM/CompPoly
Computable Polynomials in Lean.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
fpvandoorn/LeanCourse
Bonn Lean course for winter 24/25
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
Ivan-Sergeyev/Seymour
This project is about formally verifying Seymour's decomposition theorem for regular matroids.
Reservoir metadata only · declarations not indexed
verse-lab/ssreflect
LeanSSR: an SSReflect-Like Tactic Language for Lean
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
alerad/LeanCert
Verified interval arithmetic for Lean 4 - prove bounds on exp, sin, cos, find roots, all machine-checked
Reservoir metadata only · declarations not indexed
leanprover/TensorLib
A verified tensor library in Lean
Reservoir metadata only · declarations not indexed
project-numina/lib
Solving Competition Geometry Problems in Lean
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
frenzymath/reap
General neural tactic for Lean 4
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
Robby955/formal-slt
Zero-sorry Lean 4 library of finite-sample statistical learning theory: PAC-Bayes (incl. a five-component test-time meta-bound), VC, Rademacher, sharp McDiarmid, and Dudley chaining. ICML 2026 AI4MATH
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
astrainfinita/algorithm
Verified efficient algorithms in Lean4.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.