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
cameronfreer/exchangeability
Formalization of exchangeability and three proofs of de Finetti's theorem in Lean 4, following Probabilistic Symmetries and Invariance Principles by Olav Kallenberg
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
Deducteam/Lean2Dk
WIP translation from Lean to Dedukti
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
glams-lean-2024/Formal2024
Course repository for GlaMS - Formalising Mathematics in Lean (2024)
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
Hagb/lean-groebner
Lean4 formalization of Gröbner basis (WIP)
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
input-output-hk/CardanoLedgerApi
Cardano Ledger Api providing the necessary types and predicates to prove Plutus smart contracts with Blaster
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
intgrah/qdt
Query-based Dependent Type Elaborator
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
jaalonso/Calculemus2
Proof exercises in Lean4 and Isabelle/HOL
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
JamesGallicchio/Http
Basic HTTP definitions and parsing for Lean
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
keilambda/ttfpi
"Type Theory and Formal Proof: An Introduction" book formalization in Lean
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
lambdaclass/optisat
Formally verified equality saturation engine in Lean 4, parameterized by typeclasses. OptiSat provides a domain-agnostic e-graph with 248 theorems
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
leanprover/hex
Verified computational algebra in Lean 4: aggregator for the released hex libraries
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
leanprover/TenCert
Verified tensor compilation in Lean
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.