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
Koukyosyumei/pol
Proof of Lean: Formalizing Blockchain Fundamentals in Lean
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
lamafab/octra-hfhe
No package description is available.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
leanprover/sos
A Lean 4 sum-of-squares tactic for nonlinear real arithmetic.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
lexzaiello/Dcc
The dependently-typed combinator calculus (DCC).
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
lightward/foam
geometry of hospitality
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
lindy-labs/corelib_verification
No package description is available.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
Linyxus/capless
No package description is available.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
madvorak/Koch
Koch 2D snowflake generator for 4D Golf
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
mariovagomarzal/HigherCategoryTheory
A formal verification project based on the work by Enric Cosme Llópez on "Higher-order categories".
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
math-xmum/Game
Abstract Algebra Game
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
MichaelStollBayreuth/legendre_QF
Lean code formalizing a proof of Legendre's theorem on diagonal ternary quadratic forms
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
mrdouglasny/SpectralPositivity
Perron-Frobenius, Jentzsch theorem, and matrix/operator positivity in Lean 4
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.