therefore
Sign up
Open navigation

Pinned Reservoir catalog

Lean packages and dependencies

Search package metadata by name, description, keyword, license, toolchain, or dependency name. Proof-indexed projects connect to their exact Therefore declaration records.

Package records are ecosystem metadata. Build evidence appears only when Reservoir observed the exact revision and toolchain.

782 packages

782 packages pinned from Reservoir

argumentcomputer/Ipld.lean

Ipld.lean

a Lean4 implementation of the IPLD format

Reservoir metadata only · declarations not indexed

Versions
1
Declarations
Not indexed
GitHub stars
8
License
MIT

Reservoir observed an exact-toolchain build. Therefore did not run this build.

argumentcomputer/Poseidon.lean

Poseidon.lean

A Lean 4 implementation of the Poseidon zkSNARK-friendly hash function

Reservoir metadata only · declarations not indexed

Versions
1
Declarations
Not indexed
GitHub stars
8
License
MIT

Reservoir observed an exact-toolchain build. Therefore did not run this build.

avigad/LeanSudoku

LeanSudoku

Playing Sudoku in the Lean 4 proof assistant

Reservoir metadata only · declarations not indexed

Versions
1
Declarations
Not indexed
GitHub stars
8
License
Apache-2.0

Reservoir observed an exact-toolchain build. Therefore did not run this build.

CAIMEOX/json-schema

json-schema

Json Schema lean implementation

Reservoir metadata only · declarations not indexed

Versions
1
Declarations
Not indexed
GitHub stars
8
License
MIT

Reservoir observed an exact-toolchain build. Therefore did not run this build.

CBirkbeck/LeanBridge

LeanBridge

Link LMFDB and Lean

Reservoir metadata only · declarations not indexed

Versions
2
Declarations
Not indexed
GitHub stars
8
License
Apache-2.0

Reservoir observed an exact-toolchain build. Therefore did not run this build.

chrisflav/bruhat-tits

bruhat-tits

A formalisation of the Bruhat-Tits tree in Lean4

Reservoir metadata only · declarations not indexed

Versions
2
Declarations
Not indexed
GitHub stars
8
License
Apache-2.0

Reservoir observed an exact-toolchain build. Therefore did not run this build.

FormalizedFormalLogic/incompleteness

incompleteness

Formalize Incompleness Theorem Related Results

Reservoir metadata only · declarations not indexed

Versions
1
Declarations
Not indexed
GitHub stars
8
License
Apache-2.0

Reservoir observed an exact-toolchain build. Therefore did not run this build.

FredRaj3/SemicircleLaw

SemicircleLaw

Formalization of Wigner's Semicircle Law in Lean

Reservoir metadata only · declarations not indexed

Versions
2
Declarations
Not indexed
GitHub stars
8
License
MIT

Reservoir observed an exact-toolchain build. Therefore did not run this build.

girving/render

render

Verified renders of the Mandelbrot set

Reservoir metadata only · declarations not indexed

Versions
1
Declarations
Not indexed
GitHub stars
8
License
Apache-2.0

Reservoir observed an exact-toolchain build failure. Therefore did not run this build.

hanwenzhu/MillerRabin

MillerRabin

Miller–Rabin primality test in Lean

Reservoir metadata only · declarations not indexed

Versions
2
Declarations
Not indexed
GitHub stars
8
License
Apache-2.0

Reservoir observed an exact-toolchain build. Therefore did not run this build.

JadAbouHawili/Game

Game

Knights and Knaves Educational Game in Lean 4

Reservoir metadata only · declarations not indexed

Versions
1
Declarations
Not indexed
GitHub stars
8
License
MIT

Reservoir observed an exact-toolchain build. Therefore did not run this build.