Package metadataLean library
lean-units
lean physical unit system, SI international
Declarations not yet indexedLean 4.24.0
Pinned Reservoir package record · checked 2026-07-25
Math
Beyond Mathlib
The Lean research ecosystem, in one directory.
Browse 636 source-backed Lean ecosystem records from curated repositories and a pinned Reservoir snapshot. Exact Therefore declaration coverage is labelled separately from package and repository discovery.
Reservoir index b6ac225af74c backs 600 directory records. Provider metadata is discovery evidence, not proof verification or authorship.
433 of 636 projects
Clear searchPackage metadataLean library
sal
Multimodal verification of Replicated Data Types in Lean
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
Coinductive
Co-inductive datatypes for Lean
Declarations not yet indexedLean 4.32.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
sadol
Symbolic and Automatic Differentiation of Languages in Lean
Declarations not yet indexedLean 4.14.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
leanblas
Bindings and specification for BLAS
Declarations not yet indexedLean 4.28.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
vcsp
General-Valued Constraint Satisfaction Problems
Declarations not yet indexedLean 4.18.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
lean4-assert-command
A simple assertion command for Lean4
Declarations not yet indexedLean 4
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
LeanLangur
Expositions and demos for Lean Prover
Declarations not yet indexedLean 4.29.0
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
solanalib
⚠️ Experimental | Prototype
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
LiterateLean
literate programming for lean4
Declarations not yet indexedLean 4.32.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
GibbsMeasure
ASCI Summer Research Lean
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
MathMeasure TheoryProbabilityStatistical Physics
Package metadataLean library
printiest
A pretty printer for Lean 4
Declarations not yet indexedLean 4
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Lurk.lean
A Lean 4 implementation of the Lurk Language for recursive zkSNARKS
Declarations not yet indexedLean nightly-2023-01-10
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Lean2Dk
WIP translation from Lean to Dedukti
Declarations not yet indexedLean 4.22.0-rc4
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
CardanoLedgerApi
Cardano Ledger Api providing the necessary types and predicates to prove Plutus smart contracts with Blaster
Declarations not yet indexedLean 4.24.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
qdt
Query-based Dependent Type Elaborator
Declarations not yet indexedLean 4.30.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Http
Basic HTTP definitions and parsing for Lean
Declarations not yet indexedLean 4.5.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
optisat
Formally verified equality saturation engine in Lean 4, parameterized by typeclasses. OptiSat provides a domain-agnostic e-graph with 248 theorems
Declarations not yet indexedLean 4.26.0
Pinned Reservoir package record · checked 2026-07-25
E GraphEquality SaturationVerification