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

T-Brick/numbers

numbers

Arbitrary Bit-Length Integers in Lean

Reservoir metadata only · declarations not indexed

Versions
6
Declarations
Not indexed
GitHub stars
4
License
GPL-3.0

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

Th0rgal/morpho-verity

morpho-verity

Formal verification of Morpho Blue lending protocol using Verity (Lean 4)

Reservoir metadata only · declarations not indexed

Versions
1
Declarations
Not indexed
GitHub stars
4
License
MIT

todbeibrot/mrdi

mrdi

An interface between Lean4 and Oscar.

Reservoir metadata only · declarations not indexed

Versions
1
Declarations
Not indexed
GitHub stars
4
License
GPL-3.0

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

vbeffara/rMT4

rMT4

The Riemann mapping theorem

Reservoir metadata only · declarations not indexed

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

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

Verilean/lean-tea

lean-tea

No package description is available.

Reservoir metadata only · declarations not indexed

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

wvhulle/ennreal-arith

ennreal-arith

Arithmetic tactics for extended non-negative real numbers (ENNReal)

Reservoir metadata only · declarations not indexed

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

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

YaelDillies/MiscYD

MiscYD

Miscellaneous projects I am working on in Lean

Reservoir metadata only · declarations not indexed

Versions
18
Declarations
Not indexed
GitHub stars
4
License
Apache-2.0

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

yezhuoyang/LogicQ

LogicQ

An IR language for fault-tolerant quantum programming

Reservoir metadata only · declarations not indexed

Versions
1
Declarations
Not indexed
GitHub stars
4
License
MIT

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

YijunYuan/SphericalCompleteness

SphericalCompleteness

No package description is available.

Reservoir metadata only · declarations not indexed

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

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

2540825244/m2r-group-7

m2r-group-7

Classifying Groups of Order up to 31 in Lean 4 - Imperial Maths Year 2 Research Project Group 7 - 2026

Reservoir metadata only · declarations not indexed

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

adamtopaz/lean_extras

lean_extras

No package description is available.

Reservoir metadata only · declarations not indexed

Versions
1
Declarations
Not indexed
GitHub stars
3
License
MIT

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

adomani/advents

advents

Advent of Code

Reservoir metadata only · declarations not indexed

Versions
1
Declarations
Not indexed
GitHub stars
3
License
MIT

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