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
VTrelat/B
Higher-order encoder for B proof obligations to SMT-LIB 2.7
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
VTrelat/ZFLean
A practical framework for set-theoretical development in Lean
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
wupr/order-p-q
Lean formalisation of the classification of the groups of order p * q where p and q are prime numbers.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
znssong/Frucht
Formalization of Frucht's theorem in Lean
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
AdrienChampion/collChoSoWel
No package description is available.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
algebraic-dev/Colorized
🌈 | A Lean 4 library designed to enhance terminal output with vibrant ANSI escape sequences.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
arademaker/vizagrams
A visualization library for Lean
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
atlas-computing-org/coq_lean_translation
No package description is available.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
ATOMSLab/DimensionalAnalysis
Formally-verified dimensional analysis in Lean
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
Beneficial-AI-Foundation/NumpySpec
numpy -> lean 4 through ai
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
dagurtomas/LeanCondensed
No package description is available.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
dududuguo/HighDimProb
Lean 4 formalizations for high-dimensional probability, random matrices, concentration inequalities, and matrix Bernstein bounds.
Reservoir metadata only · declarations not indexed