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.

433 of 636 projects

Clear search
Package metadataLean library

CodeProofTheArena

Lean coding problem solving challenge website with proof verification

Declarations not yet indexedLean 4.14.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

lost-pop-lean

POP Memory Model in Lean

Declarations not yet indexedLean 4.30.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

cpdt-lean

Lean implementations of things found in Certified Programming with Dependent Types

Declarations not yet indexedLean nightly-2022-06-05

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

linglib

A Lean 4 library for formal linguistics: semantics, syntax, pragmatics, morphology, phonology, and processing - formalized across competing frameworks for high interconnection density.

Declarations not yet indexedLean 4.32.0

Pinned Reservoir package record · checked 2026-07-25

Formal SemanticsFormal SyntaxLinguisticsPhonology
Package metadataLean library

i18n

i18n library for Lean.

Declarations not yet indexedLean 4.31.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

PlutusCore

Plutus Core, CEK Machine in Lean 4, tailored for Blaster usage

Declarations not yet indexedLean 4.24.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

certifyingDatalog

A certified checker for Datalog entailments, written in Lean

Declarations not yet indexedLean 4.32.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

LeanSage

SageMath integration for Lean4

Declarations not yet indexedLean 4.25.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

testing_lower_bounds

Information theory and hypothesis testing, in Lean

Declarations not yet indexedLean 4.13.0-rc3

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Numbers

An introduction to numbers

Declarations not yet indexedLean 4.31.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

goose

GOOSE in Lean4

Declarations not yet indexedLean 4.22.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Http.lean

Basic Http functionality in Lean (unfinished)

Declarations not yet indexedLean nightly-2022-09-11

Pinned Reservoir package record · checked 2026-07-25

Http
Package metadataLean library

ray-series

Power series arithmetic in Lean

Declarations not yet indexedLean 4.26.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

pteffects

Effect monads with specifications (DIjkstra Monads) in Lean 4

Declarations not yet indexedLean 4.3.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Hex

Verified computational algebra in Lean 4 - polynomial factoring, LLL, and friends

Declarations not yet indexedLean 4.32.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

duality

Duality theory in linear optimization and its extensions

Declarations not yet indexedLean 4.18.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

many-sorted-model-theory

A lean repository for building many-sorted logic, with a view towards model theory of valued fields

Declarations not yet indexedLean 4.30.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

leansi

Leansi is a Lean Library for terminal formatting.

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Lean package