Package metadataLean library
pdl
Tableaux for Propositional Dynamic Logic in Lean 4 (WORK IN PROGRESS)
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
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
plonky3-example
A framework for extracting and formally verifying constraint systems from the Plonky3 zkDSL in Lean.
Declarations not yet indexedLean 4.23.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
timelib
A date and time library for Lean 4
Declarations not yet indexedLean 4.19.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Etheorem
A Lean 4 implementation of the Ethereum consensus specification for the Fulu and Gloas forks.
Declarations not yet indexedLean 4.29.1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
leanwuzla
Connecting bv_decide to SMTLIB.
Declarations not yet indexedLean nightly-2026-06-08
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
lean_reducers
Parallel, fused reducers for Lean 4
Declarations not yet indexedLean 4.30.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
povu_lean
A toolkit for exploring regions of variation in pangenomes
Declarations not yet indexedLean 4.29.1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
btc-verified
Verified Bitcoin protocol components in Lean 4 - serialization, txids, and merkle commitments checked against real mainnet blocks.
Declarations not yet indexedLean 4.30.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Algolean
Algorithms and Complexity Library using the lightweight query combinator framework called "Prog"
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
AlgorithmsComputer Science
Package metadataLean library
itertools
A Lean 4 library for iterators.
Declarations not yet indexedLean 4.3.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
fad
Functional Algorithms Design
Declarations not yet indexedLean 4.31.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
FFaCiL.lean
Finite Fields and Curves in Lean
Declarations not yet indexedLean nightly-2023-01-10
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Curl
Lean 4 bindings to libcurl
Declarations not yet indexedLean 4.27.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
clap
Implementation of the Clap language for ZK Circuits in the Lean proof-assistant
Declarations not yet indexedLean 4.29.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
bdd
Binary Decision Diagrams in Lean 4
Declarations not yet indexedLean 4.29.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
minif2f
A fork of openai/miniF2F adapted to Lean 4, with corrections to formalizations and informal descriptions. for human readers.
Declarations not yet indexedLean 4.27.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Curve25519Dalek
Verifying curve25519-dalek using Lean
Declarations not yet indexedLean 4.30.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Formal Verification
Package metadataLean library
implab
Lean playground for programming language modeling tooling.
Declarations not yet indexedLean 4.29.0
Pinned Reservoir package record · checked 2026-07-25
Lean package