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
girving/bottcher
Verified computation of the Mandelbrot set Böttcher series
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
ionathanch/CBPV
Lean 4 mechanization of assorted CBPV metatheory.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
kbuzzard/Game
An interactive game introducing the concept of a filter.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
keilambda/eocia-lean
Essentials of Compilation: An Incremental Approach in Lean 4
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
matematiflo/leanproject
GitHub repository for the seminar on Computer-assisted mathematics held at the University of Heidelberg during the Summer Semester of 2024.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
mattrobball/BridgelandStability
No package description is available.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
mgignoux/GL
Craig interpolation for GL in Lean
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
MichaelStollBayreuth/Heights
An attempt at formalizing the theory of heights in Lean
Reservoir metadata only · declarations not indexed
monsterkrampe/ExistentialRules
This repo contains formalizations around Existential Rules (aka. Tuple-Generating Dependencies) with disjunctions and the Chase algorithm. Mostly this will be about (basics of) my own formal works.
Reservoir metadata only · declarations not indexed
oOo0oOo/LeanRPC
Serve Lean 4 functions as RPC methods over HTTP
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
oOo0oOo/paranoia
Lean 4 proof verification without reference
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
or4nge19/MCMC
Formalization of Markov Chain Monte Carlo in Lean 4
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.