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
fgdorais/UnicodeBasic
Basic Unicode support for Lean 4
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
hanwenzhu/premise-selection
No package description is available.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
iasakura/lean-yjs
Lean-Yjs: Formal Verification of Yjs Integration Algorithm
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
inQWIRE/quantumlib
A Quantum Computing Library in LEAN
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
ixaxaar/monoid.space
Learn pure math with agda :rocket:
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
jsm28/IMO
Suggested conventions and examples for Lean formalization of IMO problem statements
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
kbuzzard/ClassFieldTheory
Github repository for the 2025 Clay Summer School on Formalizing Class Field Theory
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
lean-ja/lean99
These are Lean translations of Ninety-Nine Haskell Problems (WIP)
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
leanprover/verso-slides
No package description is available.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
m4lvin/pdl
Tableaux for Propositional Dynamic Logic in Lean 4 (WORK IN PROGRESS)
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
madvorak/fecssk
Formalisms Every Computer Scientist Should Know (course at ISTA)
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
NethermindEth/plonky3-example
A framework for extracting and formally verifying constraint systems from the Plonky3 zkDSL in Lean.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.