therefore
Sign up
Open navigation

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.

600 of 636 projects

Clear search
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 metadataProof corpus

real-closed-field

Formalisation of the theory of real closed fields in Lean 4.

Declarations not yet indexedLean 4.33.0-rc1

Pinned Reservoir package record · checked 2026-07-25

AlgebraMath
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 metadataProof corpus

AM

Lean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib)

Declarations not yet indexedLean 4.32.0-rc1

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 metadataProof corpus

clt

Central limit theorem in Lean

Declarations not yet indexedLean 4.29.0-rc3

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 metadataProof corpus

partial-combinatory-algebras

A Lean 4 formalization of partial combinatory algebras.

Declarations not yet indexedLean 4.15.0-rc1

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 metadataProof corpus

arithmetization

Formalization of Arithmetization of Mathematics/Metamathematics

Declarations not yet indexedLean 4.17.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package